The Stasheff identities

Given a graded R-linear quiver with higher compositions mₙ : Hom(X₀, X₁) ⊗ ⋯ ⊗ Hom(Xₙ₋₁, Xₙ) → Hom(X₀, Xₙ) of degree 2 - n, the arity-n Stasheff identity states that ∑_{r + s + t = n, s ≥ 1} (-1)^(‖a_{r+s+1}‖ + ⋯ + ‖a_n‖) m_{r+1+t}(a_1, …, a_r, m_s(a_{r+1}, …, a_{r+s}), a_{r+s+1}, …, a_n) = 0.

Main definitions

• AInfinityTheory.AInfinityComposition: the type of higher compositions mₙ on a graded linear quiver.
• AInfinityTheory.indexedStasheffTerm: the (r, s, t) summand of the Stasheff sum.
• AInfinityTheory.StasheffIndex: the index triples (r, s, t) with r + s + t = n and 1 ≤ s.
• AInfinityTheory.stasheffSign: the Koszul sign of the (r, s, t) summand.
• AInfinityTheory.signedStasheffSum: the sum of a family of (r, s, t) terms with these signs.
• AInfinityTheory.indexedStasheffSum: the signed Stasheff sum in arity n.
• AInfinityTheory.IndexedSatisfiesStasheff: the Stasheff identities in every arity.

Main results

• AInfinityTheory.indexedSatisfiesStasheff_of_arity_two: if m vanishes outside arity 2, the Stasheff identities reduce to the arity-3 one, i.e. associativity of m₂ up to sign.

@[reducible, inline]

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

Target degree of the n-ary operation m.

Equations

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

@[reducible, inline]

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

Target degree of the arity-n Stasheff relation.

Equations

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

theorem AInfinityTheory.stasheffTargetDeg_eq_operationTargetDeg_add_shift_one {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) : stasheffTargetDeg deg = operationTargetDeg deg + shift 1

The arity-n Stasheff relation has degree one more than the n-ary operation m.

structure AInfinityTheory.StasheffIndex (n : ℕ) : Type

An index triple (r, s, t) of the arity-n Stasheff identity: r + s + t = n and 1 ≤ s.

• r : ℕ

  The number of inputs before the inner operation.

• s : ℕ

  The arity of the inner operation.

• t : ℕ

  The number of inputs after the inner operation.

• sum_eq : self.r + self.s + self.t = n

  The three blocks of inputs make up all n inputs.

• one_le_s : 1 ≤ self.s

  The inner operation has at least one input.

theorem AInfinityTheory.StasheffIndex.ext_iff {n : ℕ} {x y : StasheffIndex n} : x = y ↔ x.r = y.r ∧ x.s = y.s ∧ x.t = y.t

theorem AInfinityTheory.StasheffIndex.ext {n : ℕ} {x y : StasheffIndex n} (r : x.r = y.r) (s : x.s = y.s) (t : x.t = y.t) : x = y

def AInfinityTheory.instDecidableEqStasheffIndex.decEq {n✝ : ℕ} (x✝ x✝¹ : StasheffIndex n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance AInfinityTheory.instDecidableEqStasheffIndex {n✝ : ℕ} : DecidableEq (StasheffIndex n✝)

Equations

• AInfinityTheory.instDecidableEqStasheffIndex = AInfinityTheory.instDecidableEqStasheffIndex.decEq

def AInfinityTheory.StasheffIndex.equivLt {n : ℕ} : StasheffIndex n ≃ { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 }

An index triple (r, s, t) is determined by the endpoints r < r + s of the nonempty interval of inputs fed to the inner operation.

Equations

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

@[implicit_reducible]

instance AInfinityTheory.instFintypeStasheffIndex {n : ℕ} : Fintype (StasheffIndex n)

Equations

• AInfinityTheory.instFintypeStasheffIndex = Fintype.ofEquiv { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 } AInfinityTheory.StasheffIndex.equivLt.symm

instance AInfinityTheory.instNeZeroNatS {n : ℕ} (p : StasheffIndex n) : NeZero p.s

The inner operation of a Stasheff term has positive arity.

instance AInfinityTheory.instNeZeroNatHAddROfNatT {n : ℕ} (p : StasheffIndex n) : NeZero (p.r + 1 + p.t)

The outer operation of a Stasheff term has positive arity.

@[reducible, inline]

abbrev AInfinityTheory.AInfinityComposition (β : Type v) [AddCommGroup β] [GradingType β] (R : Type u) [CommRing R] (Obj : Type w) [GradedLinearQuiver β R Obj] : Type (max (max w u_1) v)

The type of A∞ compositions on a graded linear quiver: for each arity n ≥ 1 and each composable string of objects obj, a graded multilinear map mₙ of degree 2 - n from the composable hom spaces to the hom space from obj 0 to obj (Fin.last n).

Equations

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

def AInfinityTheory.stasheffDegIn {β : Type v} {n : ℕ} (deg : Fin n → β) (p : StasheffIndex n) : Fin p.s → β

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

Equations

• AInfinityTheory.stasheffDegIn deg p j = deg (Fin.cast ⋯ (Fin.castAdd p.t (Fin.natAdd p.r j)))

def AInfinityTheory.stasheffInnerDeg {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) (p : StasheffIndex n) : β

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

Equations

• AInfinityTheory.stasheffInnerDeg deg p = AInfinityTheory.operationTargetDeg (AInfinityTheory.stasheffDegIn deg p)

def AInfinityTheory.stasheffDegOut {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) (p : StasheffIndex n) : Fin (p.r + 1 + p.t) → β

Helper: the outer degree function. It lists the degrees of the first r inputs, then the degree of the inner output, then the degrees of the last t inputs.

Equations

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

@[simp]

theorem AInfinityTheory.stasheffDegOut_left {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) (p : StasheffIndex n) (j : Fin p.r) : stasheffDegOut deg p (Fin.castAdd p.t j.castSucc) = deg (Fin.cast ⋯ (Fin.castAdd p.t (Fin.castAdd p.s j)))

On the first block, the outer degrees are the degrees of the first r inputs.

@[simp]

theorem AInfinityTheory.stasheffDegOut_middle {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) (p : StasheffIndex n) : stasheffDegOut deg p (Fin.castAdd p.t (Fin.last p.r)) = stasheffInnerDeg deg p

In the middle slot, the outer degree is the degree of the inner output.

@[simp]

theorem AInfinityTheory.stasheffDegOut_right {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) (p : StasheffIndex n) (k : Fin p.t) : stasheffDegOut deg p (Fin.natAdd (p.r + 1) k) = deg (Fin.cast ⋯ (Fin.natAdd (p.r + p.s) k))

On the last block, the outer degrees are the degrees of the last t inputs.

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

Helper: the inner object string obj r, …, obj (r + s).

Equations

• AInfinityTheory.stasheffObjIn obj p j = obj (Fin.castLE ⋯ (Fin.natAdd p.r j))

def AInfinityTheory.stasheffObjOut {n : ℕ} {Obj : Type w} (obj : Fin (n + 1) → Obj) (p : StasheffIndex n) : Fin (p.r + 1 + p.t + 1) → Obj

Helper: the outer object string obj 0, …, obj r, obj (r + s), …, obj n obtained by collapsing the inner block.

Equations

• AInfinityTheory.stasheffObjOut obj p = Fin.append (fun (j : Fin (p.r + 1)) => obj (Fin.castLE ⋯ j)) fun (k : Fin (p.t + 1)) => obj (Fin.cast ⋯ (Fin.natAdd (p.r + p.s) k))

@[simp]

theorem AInfinityTheory.stasheffObjOut_left {n : ℕ} {Obj : Type w} (obj : Fin (n + 1) → Obj) (p : StasheffIndex n) (j : Fin (p.r + 1)) : stasheffObjOut obj p (Fin.castLE ⋯ j) = obj (Fin.castLE ⋯ j)

Up to the inner block, the outer object string agrees with the original one.

@[simp]

theorem AInfinityTheory.stasheffObjOut_right {n : ℕ} {Obj : Type w} (obj : Fin (n + 1) → Obj) (p : StasheffIndex n) (k : Fin (p.t + 1)) : stasheffObjOut obj p (Fin.natAdd (p.r + 1) k) = obj (Fin.cast ⋯ (Fin.natAdd (p.r + p.s) k))

After the inner block, the outer object string agrees with the original one, shifted by s - 1.

@[simp]

theorem AInfinityTheory.stasheffObjOut_zero {n : ℕ} {Obj : Type w} (obj : Fin (n + 1) → Obj) (p : StasheffIndex n) : stasheffObjOut obj p 0 = obj 0

The outer object string starts at obj 0.

@[simp]

theorem AInfinityTheory.stasheffObjOut_last {n : ℕ} {Obj : Type w} (obj : Fin (n + 1) → Obj) (p : StasheffIndex n) : stasheffObjOut obj p (Fin.last (p.r + 1 + p.t)) = obj (Fin.last n)

The outer object string ends at obj (Fin.last n).

theorem AInfinityTheory.stasheffDegOut_sum {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) (p : StasheffIndex n) : operationTargetDeg (stasheffDegOut deg p) = stasheffTargetDeg deg

The outer operation has the Stasheff target degree.

From here on, obj and deg are inferred from the operations m and the inputs x; declarations that take neither bind them explicitly.

theorem AInfinityTheory.aInfinityComposition_homCongr_deg {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} [NeZero n] {deg deg' : Fin n → β} (hdeg : deg = deg') (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) {d : β} (hd : operationTargetDeg deg = d) (hd' : operationTargetDeg deg' = d) : ((↑(m obj) deg' d hd') fun (i : Fin n) => (GradedLinearQuiver.homCongr R ⋯ ⋯ ⋯) (x i)) = (↑(m obj) deg d hd) x

Rewriting the degree function and transporting each input does not change the value of m.

def AInfinityTheory.indexedStasheffXIn {β : Type v} {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (j : Fin p.s) : GradedLinearQuiver.ComposableHomType R (stasheffObjIn obj p) j (stasheffDegIn deg p j)

Helper: the input tuple for the inner operation in a Stasheff term.

Equations

• AInfinityTheory.indexedStasheffXIn x p j = x (Fin.cast ⋯ (Fin.castAdd p.t (Fin.natAdd p.r j)))

@[simp]

theorem AInfinityTheory.indexedStasheffXIn_apply {β : Type v} {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (j : Fin p.s) : indexedStasheffXIn x p j = x (Fin.cast ⋯ (Fin.castAdd p.t (Fin.natAdd p.r j)))

Evaluating the inner input tuple just picks out the corresponding original input.

def AInfinityTheory.indexedStasheffInner {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (d : β) (hd : stasheffInnerDeg deg p = d) : GradedLinearQuiver.Hom R (stasheffObjIn obj p 0) (stasheffObjIn obj p (Fin.last p.s)) d

Helper: the inner value appearing in a Stasheff term, in any degree d equal to the inner degree.

Equations

• AInfinityTheory.indexedStasheffInner m x p d hd = (↑(m (AInfinityTheory.stasheffObjIn obj p)) (AInfinityTheory.stasheffDegIn deg p) d hd) (AInfinityTheory.indexedStasheffXIn x p)

@[reducible, inline]

abbrev AInfinityTheory.indexedStasheffMiddleIndex {n : ℕ} (p : StasheffIndex n) : Fin (p.r + 1 + p.t)

Helper: the middle index in the outer tuple of a Stasheff term.

Equations

• AInfinityTheory.indexedStasheffMiddleIndex p = Fin.castAdd p.t (Fin.last p.r)

def AInfinityTheory.indexedStasheffXOutEquivLeft {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (R : Type u) [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (obj : Fin (n + 1) → Obj) (deg : Fin n → β) (p : StasheffIndex n) (j : Fin p.r) : GradedLinearQuiver.ComposableHomType R obj (Fin.cast ⋯ (Fin.castAdd p.t (Fin.castAdd p.s j))) (deg (Fin.cast ⋯ (Fin.castAdd p.t (Fin.castAdd p.s j)))) ≃ₗ[R] GradedLinearQuiver.ComposableHomType R (stasheffObjOut obj p) (Fin.castAdd p.t j.castSucc) (stasheffDegOut deg p (Fin.castAdd p.t j.castSucc))

Before the inserted block, the space of an original input is identified with the corresponding outer input space.

Equations

• AInfinityTheory.indexedStasheffXOutEquivLeft R obj deg p j = AInfinityTheory.GradedLinearQuiver.homCongr R ⋯ ⋯ ⋯

def AInfinityTheory.indexedStasheffXOutEquivMid {β : Type v} {n : ℕ} (R : Type u) [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (obj : Fin (n + 1) → Obj) (p : StasheffIndex n) (d : β) : GradedLinearQuiver.Hom R (stasheffObjIn obj p 0) (stasheffObjIn obj p (Fin.last p.s)) d ≃ₗ[R] GradedLinearQuiver.ComposableHomType R (stasheffObjOut obj p) (indexedStasheffMiddleIndex p) d

At the inserted block, the space of the inner output is identified with the outer middle input space, in any degree d.

Equations

• AInfinityTheory.indexedStasheffXOutEquivMid R obj p d = AInfinityTheory.GradedLinearQuiver.homCongr R ⋯ ⋯ ⋯

def AInfinityTheory.indexedStasheffXOutEquivRight {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (R : Type u) [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (obj : Fin (n + 1) → Obj) (deg : Fin n → β) (p : StasheffIndex n) (k : Fin p.t) : GradedLinearQuiver.ComposableHomType R obj (Fin.cast ⋯ (Fin.natAdd (p.r + p.s) k)) (deg (Fin.cast ⋯ (Fin.natAdd (p.r + p.s) k))) ≃ₗ[R] GradedLinearQuiver.ComposableHomType R (stasheffObjOut obj p) (Fin.natAdd (p.r + 1) k) (stasheffDegOut deg p (Fin.natAdd (p.r + 1) k))

After the inserted block, the space of an original input is identified with the corresponding outer input space.

Equations

• AInfinityTheory.indexedStasheffXOutEquivRight R obj deg p k = AInfinityTheory.GradedLinearQuiver.homCongr R ⋯ ⋯ ⋯

def AInfinityTheory.indexedStasheffXOut {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (a : Fin (p.r + 1 + p.t)) : GradedLinearQuiver.ComposableHomType R (stasheffObjOut obj p) a (stasheffDegOut deg p a)

Helper: the input tuple for the outer operation in a Stasheff term: the first r inputs, then the inner output, then the last t inputs.

Equations

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

@[simp]

theorem AInfinityTheory.indexedStasheffXOut_left {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (j : Fin p.r) : indexedStasheffXOut (fun {n : ℕ} [NeZero n] => m) x p (Fin.castAdd p.t j.castSucc) = (indexedStasheffXOutEquivLeft R obj deg p j) (x (Fin.cast ⋯ (Fin.castAdd p.t (Fin.castAdd p.s j))))

Before the inserted block, the outer input tuple agrees with the original inputs.

@[simp]

theorem AInfinityTheory.indexedStasheffXOut_right {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (k : Fin p.t) : indexedStasheffXOut (fun {n : ℕ} [NeZero n] => m) x p (Fin.natAdd (p.r + 1) k) = (indexedStasheffXOutEquivRight R obj deg p k) (x (Fin.cast ⋯ (Fin.natAdd (p.r + p.s) k)))

After the inserted block, the outer input tuple agrees with the original inputs.

@[simp]

theorem AInfinityTheory.indexedStasheffXOut_middle {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) : indexedStasheffXOut (fun {n : ℕ} [NeZero n] => m) x p (indexedStasheffMiddleIndex p) = (indexedStasheffXOutEquivMid R obj p (stasheffDegOut deg p (Fin.castAdd p.t (Fin.last p.r)))) (indexedStasheffInner (fun {n : ℕ} [NeZero n] => m) x p (stasheffDegOut deg p (Fin.castAdd p.t (Fin.last p.r))) ⋯)

The middle outer input is the transported inner output.

theorem AInfinityTheory.indexedStasheffXOut_middle_eq_zero_of_inner_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (hinner : ∀ (d : β) (hd : stasheffInnerDeg deg p = d), indexedStasheffInner (fun {n : ℕ} [NeZero n] => m) x p d hd = 0) : indexedStasheffXOut (fun {n : ℕ} [NeZero n] => m) x p (indexedStasheffMiddleIndex p) = 0

The middle outer input vanishes whenever the inner output vanishes.

def AInfinityTheory.indexedStasheffOuter {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (d : β) (hd : operationTargetDeg (stasheffDegOut deg p) = d) : GradedLinearQuiver.Hom R (stasheffObjOut obj p 0) (stasheffObjOut obj p (Fin.last (p.r + 1 + p.t))) d

Helper: the outer value appearing in a Stasheff term, in any degree d equal to the degree of the outer operation.

Equations

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

def AInfinityTheory.indexedStasheffTargetEquiv {β : Type v} {n : ℕ} (R : Type u) [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (obj : Fin (n + 1) → Obj) (p : StasheffIndex n) (d : β) : GradedLinearQuiver.Hom R (stasheffObjOut obj p 0) (stasheffObjOut obj p (Fin.last (p.r + 1 + p.t))) d ≃ₗ[R] GradedLinearQuiver.Hom R (obj 0) (obj (Fin.last n)) d

Helper: the identification of the outer target space with the final Stasheff target space, in any degree d.

Equations

• AInfinityTheory.indexedStasheffTargetEquiv R obj p d = AInfinityTheory.GradedLinearQuiver.homCongr R ⋯ ⋯ ⋯

def AInfinityTheory.indexedStasheffTerm {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (d : β) (hd : stasheffTargetDeg deg = d) : GradedLinearQuiver.Hom R (obj 0) (obj (Fin.last n)) d

A generic Stasheff term builder for object-indexed A∞ operations, in any degree d equal to the Stasheff target degree.

Equations

• AInfinityTheory.indexedStasheffTerm m x p d hd = (AInfinityTheory.indexedStasheffTargetEquiv R obj p d) (AInfinityTheory.indexedStasheffOuter (fun {n : ℕ} [NeZero n] => m) x p d ⋯)

theorem AInfinityTheory.indexedStasheffInner_eq_zero_of_map_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (hm : ∀ (d : β) (hd : ∑ j : Fin p.s, stasheffDegIn deg p j + shift (2 - ↑p.s) = d), ↑(m (stasheffObjIn obj p)) (stasheffDegIn deg p) d hd = 0) (d : β) (hd : stasheffInnerDeg deg p = d) : indexedStasheffInner (fun {n : ℕ} [NeZero n] => m) x p d hd = 0

The inner value vanishes if the inner multilinear map itself vanishes.

theorem AInfinityTheory.indexedStasheffOuter_eq_zero_of_map_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (hm : ∀ (d : β) (hd : ∑ j : Fin (p.r + 1 + p.t), stasheffDegOut deg p j + shift (2 - ↑(p.r + 1 + p.t)) = d), ↑(m (stasheffObjOut obj p)) (stasheffDegOut deg p) d hd = 0) (d : β) (hd : operationTargetDeg (stasheffDegOut deg p) = d) : indexedStasheffOuter (fun {n : ℕ} [NeZero n] => m) x p d hd = 0

The outer value vanishes if the outer multilinear map itself vanishes.

theorem AInfinityTheory.indexedStasheffOuter_eq_zero_of_inner_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (hinner : ∀ (d : β) (hd : stasheffInnerDeg deg p = d), indexedStasheffInner (fun {n : ℕ} [NeZero n] => m) x p d hd = 0) (d : β) (hd : operationTargetDeg (stasheffDegOut deg p) = d) : indexedStasheffOuter (fun {n : ℕ} [NeZero n] => m) x p d hd = 0

The outer value vanishes whenever the inserted inner output vanishes.

theorem AInfinityTheory.indexedStasheffTerm_eq_zero_iff_outer_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (d : β) (hd : stasheffTargetDeg deg = d) : indexedStasheffTerm (fun {n : ℕ} [NeZero n] => m) x p d hd = 0 ↔ indexedStasheffOuter (fun {n : ℕ} [NeZero n] => m) x p d ⋯ = 0

The final transported Stasheff term vanishes exactly when the outer value vanishes.

theorem AInfinityTheory.indexedStasheffTerm_eq_zero_of_outer_map_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (hm : ∀ (d : β) (hd : ∑ j : Fin (p.r + 1 + p.t), stasheffDegOut deg p j + shift (2 - ↑(p.r + 1 + p.t)) = d), ↑(m (stasheffObjOut obj p)) (stasheffDegOut deg p) d hd = 0) (d : β) (hd : stasheffTargetDeg deg = d) : indexedStasheffTerm (fun {n : ℕ} [NeZero n] => m) x p d hd = 0

The final Stasheff term vanishes if the outer multilinear map vanishes.

theorem AInfinityTheory.indexedStasheffTerm_eq_zero_of_inner_map_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (hm : ∀ (d : β) (hd : ∑ j : Fin p.s, stasheffDegIn deg p j + shift (2 - ↑p.s) = d), ↑(m (stasheffObjIn obj p)) (stasheffDegIn deg p) d hd = 0) (d : β) (hd : stasheffTargetDeg deg = d) : indexedStasheffTerm (fun {n : ℕ} [NeZero n] => m) x p d hd = 0

The final Stasheff term vanishes if the inner multilinear map vanishes.

def AInfinityTheory.stasheffSign {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) (p : StasheffIndex n) : ℤˣ

The Koszul sign (-1)^(‖a_{r+s+1}‖ + ⋯ + ‖a_n‖) of the Stasheff term indexed by p = (r, s, t), where ‖a‖ = |a| - 1 is the reduced degree of an input after the inner operation.

Equations

• AInfinityTheory.stasheffSign deg p = ∏ k : Fin p.t, AInfinityTheory.sign (deg (Fin.cast ⋯ (Fin.natAdd (p.r + p.s) k)) - AInfinityTheory.shift 1)

def AInfinityTheory.signedStasheffSum {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} (deg : Fin n → β) {M : Type u_1} [AddCommGroup M] (f : StasheffIndex n → M) : M

The signed sum ∑_{r + s + t = n, s ≥ 1} (-1)^(‖a_{r+s+1}‖ + ⋯ + ‖a_n‖) f (r, s, t) over the index triples StasheffIndex n of the arity-n Stasheff identity. Both the Stasheff identities and the A∞-functor equations are sums of this form.

Equations

• AInfinityTheory.signedStasheffSum deg f = ∑ q : AInfinityTheory.StasheffIndex n, AInfinityTheory.stasheffSign deg q • f q

theorem AInfinityTheory.signedStasheffSum_eq_zero {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {deg : Fin n → β} {M : Type u_1} [AddCommGroup M] {f : StasheffIndex n → M} (h : ∀ (q : StasheffIndex n), f q = 0) : signedStasheffSum deg f = 0

A signed Stasheff sum of vanishing terms vanishes.

theorem AInfinityTheory.map_signedStasheffSum {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {deg : Fin n → β} {M : Type u_1} {N : Type u_2} {G : Type u_3} [AddCommGroup M] [AddCommGroup N] [FunLike G M N] [AddMonoidHomClass G M N] (g : G) (f : StasheffIndex n → M) : g (signedStasheffSum deg f) = signedStasheffSum deg fun (q : StasheffIndex n) => g (f q)

Additive maps commute with signed Stasheff sums.

def AInfinityTheory.indexedStasheffSum {β : Type v} [AddCommGroup β] [GradingType β] {n : ℕ} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (d : β) (hd : stasheffTargetDeg deg = d) : GradedLinearQuiver.Hom R (obj 0) (obj (Fin.last n)) d

The full Stasheff sum in arity n, with Koszul signs, in any degree d equal to the Stasheff target degree.

Equations

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

def AInfinityTheory.IndexedSatisfiesStasheff {β : Type v} [AddCommGroup β] [GradingType β] {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) : Prop

The Stasheff identities for object-indexed A∞ operations.

Equations

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

theorem AInfinityTheory.indexedStasheffTerm_eq_zero_of_arity_ne_two {β : Type v} [AddCommGroup β] [GradingType β] {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) (hm : ∀ (k : ℕ) [inst : NeZero k], k ≠ 2 → ∀ (obj : Fin (k + 1) → Obj), m obj = 0) {n : ℕ} {obj : Fin (n + 1) → Obj} {deg : Fin n → β} (x : (i : Fin n) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (p : StasheffIndex n) (h2 : p.s ≠ 2 ∨ p.r + 1 + p.t ≠ 2) (d : β) (hd : stasheffTargetDeg deg = d) : indexedStasheffTerm (fun {n : ℕ} [NeZero n] => m) x p d hd = 0

If m vanishes outside arity 2, a Stasheff term vanishes unless both its inner and its outer operation are binary.

theorem AInfinityTheory.indexedSatisfiesStasheff_of_arity_two {β : Type v} [AddCommGroup β] [GradingType β] {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (m : AInfinityComposition β R Obj) (hm : ∀ (k : ℕ) [inst : NeZero k], k ≠ 2 → ∀ (obj : Fin (k + 1) → Obj), m obj = 0) (h3 : ∀ (obj : Fin (3 + 1) → Obj) (deg : Fin 3 → β) (x : (i : Fin 3) → GradedLinearQuiver.ComposableHomType R obj i (deg i)) (d : β) (hd : stasheffTargetDeg deg = d), stasheffSign deg { r := 0, s := 2, t := 1, sum_eq := ⋯, one_le_s := indexedSatisfiesStasheff_of_arity_two._proof_1 } • indexedStasheffTerm (fun {n : ℕ} [NeZero n] => m) x { r := 0, s := 2, t := 1, sum_eq := ⋯, one_le_s := indexedSatisfiesStasheff_of_arity_two._proof_1 } d hd + indexedStasheffTerm (fun {n : ℕ} [NeZero n] => m) x { r := 1, s := 2, t := 0, sum_eq := ⋯, one_le_s := indexedSatisfiesStasheff_of_arity_two._proof_1 } d hd = 0) : IndexedSatisfiesStasheff fun {n : ℕ} [NeZero n] => m

If m vanishes outside arity 2, the Stasheff identities reduce to the one in arity 3, ±m₂(m₂(a₁, a₂), a₃) + m₂(a₁, m₂(a₂, a₃)) = 0.