@[reducible, inline]

abbrev AInfinityTheory.operationTargetDeg {β : Type v} [Grading β] {n : ℕ} (deg : Fin n → β) : β

Target degree of the n-ary operation m.

Equations

• AInfinityTheory.operationTargetDeg deg = ∑ i : Fin n, deg i + AInfinityTheory.shift_ofInt (2 - ↑n)

@[reducible, inline]

abbrev AInfinityTheory.stasheffTargetDeg {β : Type v} [Grading β] {n : ℕ} (deg : Fin n → β) : β

Target degree of the arity-n Stasheff relation.

Equations

• AInfinityTheory.stasheffTargetDeg deg = ∑ i : Fin n, deg i + AInfinityTheory.shift_ofInt (3 - ↑n)

@[reducible, inline]

abbrev AInfinityTheory.validStasheffIndices (n r s : ℕ) : Prop

Equations

• AInfinityTheory.validStasheffIndices n r s = (1 ≤ s ∧ r + s ≤ n)

@[reducible, inline]

abbrev AInfinityTheory.composableHomType {β : Type v} {R : Type u} [CommRing R] {Obj : Type w} (Hom : Obj → Obj → GradedRModule R) {n : ℕ} (obj : Fin (n + 1) → Obj) (deg : Fin n → β) (i : Fin n) : ModuleCat R

The type of the i-th morphism in a composable string of objects and degrees.

Equations

• AInfinityTheory.composableHomType Hom obj deg i = Hom (obj ⟨↑i, ⋯⟩) (obj ⟨↑i + 1, ⋯⟩) (deg i)

@[reducible, inline]

abbrev AInfinityTheory.operationTargetType {β : Type v} [Grading β] {R : Type u} [CommRing R] {Obj : Type w} (Hom : Obj → Obj → GradedRModule R) {n : ℕ} (obj : Fin (n + 1) → Obj) (deg : Fin n → β) : ModuleCat R

The target type of the n-ary operation on a composable string.

Equations

• AInfinityTheory.operationTargetType Hom obj deg = Hom (obj 0) (obj (Fin.last n)) (AInfinityTheory.operationTargetDeg deg)

def AInfinityTheory.stasheffDegIn {β : Type v} {n : ℕ} (deg : Fin n → β) (r s : ℕ) (hr : r + s ≤ n) : Fin s → β

Helper: degree function for the inner portion of the Stasheff composition.

Equations

• AInfinityTheory.stasheffDegIn deg r s hr i = deg ⟨r + ↑i, ⋯⟩

def AInfinityTheory.stasheffInnerDeg {β : Type v} [Grading β] {n : ℕ} (deg : Fin n → β) (r s : ℕ) (hr : r + s ≤ n) : β

Helper: inner degree (the degree of the result of the inner multilinear map).

Equations

• AInfinityTheory.stasheffInnerDeg deg r s hr = AInfinityTheory.operationTargetDeg (AInfinityTheory.stasheffDegIn deg r s hr)

def AInfinityTheory.stasheffDegOut {β : Type v} [Grading β] {n : ℕ} (deg : Fin n → β) (r s : ℕ) (hr : r + s ≤ n) : Fin (n + 1 - s) → β

Helper: the outer degree function.

Equations

• AInfinityTheory.stasheffDegOut deg r s hr i = if h1 : ↑i < r then deg ⟨↑i, ⋯⟩ else if x : ↑i = r then AInfinityTheory.stasheffInnerDeg deg r s hr else deg ⟨↑i + s - 1, ⋯⟩

def AInfinityTheory.stasheffObjIn {n : ℕ} {Obj : Type w} (obj : Fin (n + 1) → Obj) (r s : ℕ) (hr : r + s ≤ n) : Fin (s + 1) → Obj

Helper: the inner object string.

Equations

• AInfinityTheory.stasheffObjIn obj r s hr i = obj ⟨r + ↑i, ⋯⟩

def AInfinityTheory.stasheffObjOut {n : ℕ} {Obj : Type w} (obj : Fin (n + 1) → Obj) (r s : ℕ) (hr : r + s ≤ n) : Fin (n + 1 - s + 1) → Obj

Helper: the outer object string obtained by collapsing the inner block.

Equations

• AInfinityTheory.stasheffObjOut obj r s hr i = if h1 : ↑i ≤ r then obj ⟨↑i, ⋯⟩ else obj ⟨↑i + s - 1, ⋯⟩

theorem AInfinityTheory.shift_ofInt_combine {β : Type v} [Grading β] {n s : ℕ} (hsn : s ≤ n) : shift_ofInt (2 - ↑s) + shift_ofInt (2 - ↑(n + 1 - s)) = shift_ofInt (3 - ↑n)

theorem AInfinityTheory.validStasheffIndices_of_mem_ranges {n r s : ℕ} (hr : r ∈ Finset.range (n + 1)) (hs : s ∈ Finset.Ico 1 (n - r + 1)) : validStasheffIndices n r s

theorem AInfinityTheory.stasheffDegOut_sum_core {β : Type v} [Grading β] {n : ℕ} (deg : Fin n → β) (r s : ℕ) (hr : r + s ≤ n) : ∑ i : Fin (n + 1 - s), stasheffDegOut deg r s hr i = ∑ i : Fin n, deg i + shift_ofInt (2 - ↑s)

Summing the outer degrees recovers the original total degree plus the inner shift.

theorem AInfinityTheory.stasheffDegOut_sum {β : Type v} [Grading β] {n : ℕ} (deg : Fin n → β) (r s : ℕ) (hr : r + s ≤ n) : ∑ i : Fin (n + 1 - s), stasheffDegOut deg r s hr i + shift_ofInt (2 - ↑(n + 1 - s)) = stasheffTargetDeg deg

The outer operation has the Stasheff target degree.

def AInfinityTheory.indexedStasheffTerm {β : Type v} [Grading β] {R : Type u} [CommRing R] {Obj : Type w} (Hom : Obj → Obj → GradedRModule R) (m : {n : ℕ+} → (obj : Fin (↑n + 1) → Obj) → (deg : Fin ↑n → β) → MultilinearMap R (fun (i : Fin ↑n) => ↑(composableHomType Hom obj deg i)) ↑(operationTargetType Hom obj deg)) {n : ℕ+} (obj : Fin (↑n + 1) → Obj) (deg : Fin ↑n → β) (x : (i : Fin ↑n) → ↑(composableHomType Hom obj deg i)) (r s : ℕ) (hs : 1 ≤ s) (hr : r + s ≤ ↑n) : ↑(Hom (obj 0) (obj (Fin.last ↑n)) (stasheffTargetDeg deg))

A generic Stasheff term builder for object-indexed A∞ operations.

Equations

• One or more equations did not get rendered due to their size.

def AInfinityTheory.stasheffSignParity {β : Type v} [Grading β] {n : ℕ} (deg : Fin n → β) (r s : ℕ) (hr : r + s ≤ n) : Parity

The sign parity for the (r,s) Stasheff term: sign(deg(r+s)) + ⋯ + sign(deg(n-1)) - (n-r-s) in ZMod 2.

Equations

• AInfinityTheory.stasheffSignParity deg r s hr = ∑ i : Fin (n - r - s), AInfinityTheory.Grading.sign (deg ⟨r + s + ↑i, ⋯⟩) - ↑(n - r - s)

def AInfinityTheory.stasheffSign {β : Type v} [Grading β] {n : ℕ} (deg : Fin n → β) (r s : ℕ) (hr : r + s ≤ n) : ℤ

The sign (-1)^(|a_{r+s+1}| + ⋯ + |a_n| - t) as an integer, for a valid Stasheff index pair.

Equations

• AInfinityTheory.stasheffSign deg r s hr = (-1) ^ ZMod.val (AInfinityTheory.stasheffSignParity deg r s hr)

def AInfinityTheory.indexedStasheffSum {β : Type v} [Grading β] {R : Type u} [CommRing R] {Obj : Type w} (Hom : Obj → Obj → GradedRModule R) (m : {n : ℕ+} → (obj : Fin (↑n + 1) → Obj) → (deg : Fin ↑n → β) → MultilinearMap R (fun (i : Fin ↑n) => ↑(composableHomType Hom obj deg i)) ↑(operationTargetType Hom obj deg)) {n : ℕ+} (obj : Fin (↑n + 1) → Obj) (deg : Fin ↑n → β) (x : (i : Fin ↑n) → ↑(composableHomType Hom obj deg i)) : ↑(Hom (obj 0) (obj (Fin.last ↑n)) (stasheffTargetDeg deg))

The full Stasheff sum in arity n, with Koszul signs.

Equations

• One or more equations did not get rendered due to their size.

def AInfinityTheory.indexedSatisfiesStasheff {β : Type v} [Grading β] {R : Type u} [CommRing R] {Obj : Type w} (Hom : Obj → Obj → GradedRModule R) (m : {n : ℕ+} → (obj : Fin (↑n + 1) → Obj) → (deg : Fin ↑n → β) → MultilinearMap R (fun (i : Fin ↑n) => ↑(composableHomType Hom obj deg i)) ↑(operationTargetType Hom obj deg)) : Prop

The Stasheff identities for object-indexed A∞ operations.

Equations

• One or more equations did not get rendered due to their size.