The Stasheff identities and the suspension sign

An A∞ algebra has operations mₙ : A^{⊗ n} ⟶ A of degree 2 - n subject to the Stasheff identities: for every n,

∑_{n = r + s + t, s ≥ 1} (-1) ^ (r + s * t) m_{r + 1 + t} (1^{⊗ r} ⊗ m_s ⊗ 1^{⊗ t}) = 0.  (SIₙ)

The primary encoding of these identities is the suspended one: writing sA for the shift of A and bₙ for the operations associated to mₙ, every bₙ has degree one and the identities lose their structural coefficient,

∑_{n = r + s + t, s ≥ 1} b_{r + 1 + t} (1^{⊗ r} ⊗ b_s ⊗ 1^{⊗ t}) = 0.

This file constructs both sums and proves that they agree up to one global sign, so that either vanishes exactly when the other does. Following the cited Getzler--Jones/Keller convention, the definition adopts the sign prescribed by the Koszul rule for the suspension square: because s has degree -1, its tensor power contributes (-1) ^ (∑ i, (n - 1 - i) * d i). The tensor power itself is not formalized here. Its exponent is MultilinearMap.suspExp, and TauCeti.AInfinity.suspendedStasheffTerm_eq_smul proves that the two corresponding Stasheff terms differ by this same sign for every decomposition n = p + s + t.

Both sides also carry the Koszul coefficient of the inserted operation crossing the prefix inputs, (-1) ^ ((2 - s) * (d 0 + ⋯ + d (r - 1))) before suspension and (-1) ^ ((d 0 - 1) + ⋯ + (d (r - 1) - 1)) after; these are the coefficients of MultilinearMap.koszulSign. As in TauCeti/LinearAlgebra/Graded/Insertion.lean, the degrees of the inputs are supplied as an explicit parameter rather than read off a direct-sum decomposition; on the intended component the sign is a scalar, and TauCeti.AInfinity.replaceBlock_mem_replaceDeg_of_mem_blockDeg proves that the supplied degrees are the actual ones once the inputs and the inserted value are homogeneous of the recorded degrees.

The arities one to four are written out on the nose using the supplied degree family d; these formulas themselves make no homogeneity assumption. Homogeneity enters only in evalNat_mem_blockDeg and replaceBlock_mem_replaceDeg_of_mem_blockDeg. The degeneration to a differential graded algebra is also checked.

Inputs are indexed by ℕ rather than by Fin n throughout; only the first n entries of an input family are read, and this keeps the reindexing of the Stasheff sums free of transports between propositionally equal arities.

Main definitions

• TauCeti.AInfinity.blockDeg and TauCeti.AInfinity.replaceDeg: record the degree resulting from collapsing an input block.
• TauCeti.AInfinity.stasheffTerm and TauCeti.AInfinity.suspendedStasheffTerm: the (p, s, t) term of the unsuspended and suspended Stasheff identities.
• TauCeti.AInfinity.stasheffSum and TauCeti.AInfinity.suspendedStasheffSum: the two sides of (SIₙ).

Main results

• TauCeti.AInfinity.suspExp_replaceDeg: the sign identity behind the whole comparison; the two exponents differ by the suspension sign of the whole arity, up to an even number.
• TauCeti.AInfinity.suspendedStasheffTerm_eq_smul and TauCeti.AInfinity.suspendedStasheffSum_eq_smul: a suspended term, and hence the suspended sum, is the unsuspended one scaled by that sign.
• TauCeti.AInfinity.suspendedStasheffSum_eq_zero_iff: the suspended identity free of the structural coefficient (-1) ^ (r + s * t) holds exactly when the unsuspended identity does.
• TauCeti.AInfinity.stasheffTerm_eq_zero_of_inner_eq_zero, TauCeti.AInfinity.stasheffTerm_eq_zero_of_outer_eq_zero and TauCeti.AInfinity.stasheffTerm_of_even: a term vanishes with either of its operations, and an even inner arity s leaves only the sign (-1) ^ p.
• TauCeti.AInfinity.sum_stasheff_reflect: the reflection (p, s, t) ↦ (t, s, p) of the decompositions indexing a Stasheff sum.
• TauCeti.AInfinity.stasheffSum_one, TauCeti.AInfinity.stasheffSum_two, TauCeti.AInfinity.stasheffSum_three and TauCeti.AInfinity.stasheffSum_four: the four identities written out using the supplied degree family.
• TauCeti.AInfinity.stasheffSum_two_eq_zero_iff, TauCeti.AInfinity.stasheffSum_three_eq_zero_iff_of_m_three_eq_zero and TauCeti.AInfinity.stasheffSum_four_eq_zero_of_m_three_eq_zero_of_m_four_eq_zero: the differential graded degeneration.

This advances TauCetiRoadmap/DGAInfinity/README.md, Layer 0, item "signed graded multilinear and tensor-coalgebra infrastructure", specifically "Implement the suspension/unsuspension equivalence fixed above. Prove the general Stasheff component formula and the arity 1--4 equations verbatim." The sign prescribed by the suspension square is adopted in TauCeti/LinearAlgebra/Graded/Shift.lean; its tensor power is not yet formalized. This file proves the resulting Stasheff comparison and identities. What the roadmap's acceptance test still owes is the identification of (SIₙ) with the arity-n component of b ∘ b = 0 on the bar coalgebra of TauCeti/LinearAlgebra/TensorCoalgebra/, which needs the graded, signed coderivations of that coalgebra.

References

• E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Sections 1--2, for the suspension and brace signs.
• B. Keller, Introduction to A-infinity algebras and modules, Sections 3.1 and 3.6, for the degree 2 - n, the coefficient (-1) ^ (r + s * t) and the degree -1 suspension.

theorem TauCeti.evalNat_replaceBlock_smul {u : ℕ} {N : Type uN} {R : Type uR} {A : Type uA} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid N] [Module R N] (f : MultilinearMap R (fun (x : Fin u) => A) N) (x : ℕ → A) {p : ℕ} (s : ℕ) (hp : p < u) (c : R) (v : A) : f.evalNat (replaceBlock x p s (c • v)) = c • f.evalNat (replaceBlock x p s v)

Evaluating an operation on a tuple whose replaced entry is scaled scales the value: the replaced entry sits in a single slot, in which the operation is linear.

Evaluation of suspended operations

@[simp]

theorem TauCeti.AInfinity.evalNat_suspend {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] {k : ℕ} {N : Type uN} [AddCommMonoid N] [Module R N] (d : ℕ → ℤ) (f : MultilinearMap R (fun (x : Fin k) => A) N) (x : ℕ → A) : (MultilinearMap.suspend d f).evalNat x = negOnePowCast R (MultilinearMap.suspExp k d) • f.evalNat x

The degrees of a substituted tuple

def TauCeti.AInfinity.blockDeg (d : ℕ → ℤ) (p s : ℕ) : ℤ

The degree of the value of an arity-s operation of degree 2 - s on the block of inputs of degrees d at position p.

Equations

• TauCeti.AInfinity.blockDeg d p s = ∑ j ∈ Finset.range s, d (p + j) + 2 - ↑s

theorem TauCeti.AInfinity.blockDeg_def (d : ℕ → ℤ) (p s : ℕ) : blockDeg d p s = ∑ j ∈ Finset.range s, d (p + j) + 2 - ↑s

The defining expression for the degree of a collapsed block.

def TauCeti.AInfinity.replaceDeg (d : ℕ → ℤ) (p s : ℕ) : ℕ → ℤ

The degrees of the inputs of the outer operation of a Stasheff term: the block of s degrees at position p is replaced by the degree of the value of the inner operation on it.

Equations

• TauCeti.AInfinity.replaceDeg d p s = TauCeti.replaceBlock d p s (TauCeti.AInfinity.blockDeg d p s)

@[simp]

theorem TauCeti.AInfinity.replaceDeg_of_lt (d : ℕ → ℤ) (p s : ℕ) {i : ℕ} (h : i < p) : replaceDeg d p s i = d i

@[simp]

theorem TauCeti.AInfinity.replaceDeg_self (d : ℕ → ℤ) (p s : ℕ) : replaceDeg d p s p = blockDeg d p s

@[simp]

theorem TauCeti.AInfinity.replaceDeg_of_gt (d : ℕ → ℤ) (p s : ℕ) {i : ℕ} (h : p < i) : replaceDeg d p s i = d (i + s - 1)

theorem TauCeti.AInfinity.suspExp_replaceDeg (d : ℕ → ℤ) (p s t : ℕ) : MultilinearMap.suspExp (p + 1 + t) (replaceDeg d p s) = ↑p + ↑s * ↑t + (2 - ↑s) * ∑ i ∈ Finset.range p, d i + MultilinearMap.suspExp (p + s + t) d + 2 * (↑t - ↑p - ↑s * ↑t) - ∑ i ∈ Finset.range p, (d i - 1) - MultilinearMap.suspExp s fun (j : ℕ) => d (p + j)

The suspension sign identity. Writing an arity of p + s + t as a prefix of length p, an inner block of length s and a suffix of length t, the exponent collected on the suspended side of a Stasheff term -- the Koszul sign of the degree-one operation b_s crossing the suspended prefix, plus the two suspension signs of b_s and of the outer b_{p+1+t} -- differs from the exponent collected on the unsuspended side -- the structural coefficient (-1) ^ (p + st) and the Koszul sign of m_s crossing the prefix -- by the suspension sign of the whole arity, up to an even number.

This is the computation which turns the suspended identity without the structural coefficient into the identity with the coefficient (-1) ^ (r + s * t).

The Stasheff identities

theorem TauCeti.AInfinity.sum_stasheff_reflect {M : Type u_1} [AddCommMonoid M] (n : ℕ) (f : ℕ → ℕ → ℕ → M) : ∑ p ∈ Finset.range (n + 1), ∑ s ∈ Finset.Icc 1 (n - p), f p s (n - p - s) = ∑ p ∈ Finset.range (n + 1), ∑ s ∈ Finset.Icc 1 (n - p), f (n - p - s) s p

Pass between the decompositions p + s + t and t + s + p of an arity-n Stasheff sum.

def TauCeti.AInfinity.stasheffTerm {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (p s t : ℕ) : A

The (p, s, t) term of the unsuspended Stasheff identity in arity p + s + t: the arity-s operation is substituted into the p-th slot of the arity-p + 1 + t operation. Its sign is the structural Stasheff coefficient (-1) ^ (p + s * t) together with the Koszul coefficient (-1) ^ ((2 - s) * (d 0 + ⋯ + d (p - 1))) of the degree-2 - s operation m_s crossing the p prefix inputs.

Equations

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

theorem TauCeti.AInfinity.stasheffTerm_def {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (p s t : ℕ) : stasheffTerm m d x p s t = negOnePowCast R (↑p + ↑s * ↑t + (2 - ↑s) * ∑ i ∈ Finset.range p, d i) • (m (p + 1 + t)).evalNat (replaceBlock x p s ((m s).evalNat fun (j : ℕ) => x (p + j)))

The defining expression for an unsuspended Stasheff term.

theorem TauCeti.AInfinity.stasheffTerm_eq_smul_signedOneSlot {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (p s t : ℕ) : stasheffTerm m d x p s t = negOnePowCast R (↑p + ↑s * ↑t) • (MultilinearMap.signedOneSlot (2 - ↑s) (fun (i : Fin p) => d ↑i) (MultilinearMap.domDomCongr (Fin.oneSlotEquiv p t).symm (m (p + 1 + t))) (m s)) fun (i : Fin p ⊕ Fin s ⊕ Fin t) => x ↑((Fin.blockEquiv p s t) i)

Up to the structural coefficient (-1) ^ (p + s * t), a Stasheff term is the existing signed one-slot substitution evaluated after the canonical reindexing of its three input blocks.

theorem TauCeti.AInfinity.stasheffTerm_congr {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) {e : ℕ → ℤ} {y : ℕ → A} (p s t : ℕ) (hd : ∀ i < p + s + t, d i = e i) (hx : ∀ i < p + s + t, x i = y i) : stasheffTerm m d x p s t = stasheffTerm m e y p s t

A Stasheff term only reads the degrees and inputs below its total arity.

theorem TauCeti.AInfinity.stasheffTerm_eq_zero_of_inner_eq_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) {p s t : ℕ} (h : m s = 0) : stasheffTerm m d x p s t = 0

A Stasheff term vanishes when its inner operation, of arity s, is zero.

theorem TauCeti.AInfinity.stasheffTerm_eq_zero_of_outer_eq_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) {p s t : ℕ} (h : m (p + 1 + t) = 0) : stasheffTerm m d x p s t = 0

A Stasheff term vanishes when its outer operation, of arity p + 1 + t, is zero.

theorem TauCeti.AInfinity.stasheffTerm_of_even {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) {s : ℕ} (hs : Even s) (p t : ℕ) : stasheffTerm m d x p s t = negOnePowCast R ↑p • (m (p + 1 + t)).evalNat (replaceBlock x p s ((m s).evalNat fun (j : ℕ) => x (p + j)))

When the inner arity s is even, the sign of a Stasheff term is (-1) ^ p: both the structural exponent s * t and the Koszul exponent (2 - s) * (d 0 + ⋯ + d (p - 1)) are even.

def TauCeti.AInfinity.suspendedStasheffTerm {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (p s t : ℕ) : A

The (p, s, t) term of the suspended Stasheff identity: the same substitution performed with the suspended operations, with no structural coefficient and with the Koszul coefficient of the degree-one operation b_s crossing the p suspended prefix inputs, whose degrees are d i - 1.

Equations

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

theorem TauCeti.AInfinity.suspendedStasheffTerm_def {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (p s t : ℕ) : suspendedStasheffTerm m d x p s t = negOnePowCast R (∑ i ∈ Finset.range p, (d i - 1)) • (MultilinearMap.suspend (replaceDeg d p s) (m (p + 1 + t))).evalNat (replaceBlock x p s ((MultilinearMap.suspend (fun (j : ℕ) => d (p + j)) (m s)).evalNat fun (j : ℕ) => x (p + j)))

The defining expression for a suspended Stasheff term.

def TauCeti.AInfinity.stasheffSum {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (n : ℕ) : A

The left-hand side (SI_n) of the arity-n Stasheff identity: the sum of TauCeti.AInfinity.stasheffTerm over the decompositions n = p + s + t with 1 ≤ s.

Equations

• TauCeti.AInfinity.stasheffSum m d x n = ∑ p ∈ Finset.range (n + 1), ∑ s ∈ Finset.Icc 1 (n - p), TauCeti.AInfinity.stasheffTerm m d x p s (n - p - s)

theorem TauCeti.AInfinity.stasheffSum_def {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (n : ℕ) : stasheffSum m d x n = ∑ p ∈ Finset.range (n + 1), ∑ s ∈ Finset.Icc 1 (n - p), stasheffTerm m d x p s (n - p - s)

The defining double sum for the unsuspended Stasheff identity.

@[simp]

theorem TauCeti.AInfinity.stasheffSum_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) : stasheffSum m d x 0 = 0

def TauCeti.AInfinity.suspendedStasheffSum {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (n : ℕ) : A

The left-hand side of the arity-n Stasheff identity in the suspended encoding: the sum of TauCeti.AInfinity.suspendedStasheffTerm over the same decompositions n = p + s + t, with no structural coefficient. Its identification with the arity-n component of b ∘ b on the bar coalgebra belongs to the tensor-coalgebra layer and is not proved here.

Equations

• TauCeti.AInfinity.suspendedStasheffSum m d x n = ∑ p ∈ Finset.range (n + 1), ∑ s ∈ Finset.Icc 1 (n - p), TauCeti.AInfinity.suspendedStasheffTerm m d x p s (n - p - s)

theorem TauCeti.AInfinity.suspendedStasheffSum_def {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (n : ℕ) : suspendedStasheffSum m d x n = ∑ p ∈ Finset.range (n + 1), ∑ s ∈ Finset.Icc 1 (n - p), suspendedStasheffTerm m d x p s (n - p - s)

The defining double sum for the suspended Stasheff identity.

theorem TauCeti.AInfinity.suspendedStasheffSum_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) : suspendedStasheffSum m d x 0 = 0

@[simp]

theorem TauCeti.AInfinity.suspendedStasheffTerm_eq_smul {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (p s t : ℕ) : suspendedStasheffTerm m d x p s t = negOnePowCast R (MultilinearMap.suspExp (p + s + t) d) • stasheffTerm m d x p s t

The suspended and unsuspended Stasheff terms agree up to the suspension sign of the whole arity. The sign does not depend on the decomposition, which is why the two identities are equivalent.

theorem TauCeti.AInfinity.suspendedStasheffTerm_congr {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) {e : ℕ → ℤ} {y : ℕ → A} (p s t : ℕ) (hd : ∀ i < p + s + t, d i = e i) (hx : ∀ i < p + s + t, x i = y i) : suspendedStasheffTerm m d x p s t = suspendedStasheffTerm m e y p s t

A suspended Stasheff term only reads the degrees and inputs below its total arity.

theorem TauCeti.AInfinity.stasheffSum_congr {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) {e : ℕ → ℤ} {y : ℕ → A} (n : ℕ) (hd : ∀ i < n, d i = e i) (hx : ∀ i < n, x i = y i) : stasheffSum m d x n = stasheffSum m e y n

The arity-n Stasheff sum only reads the first n supplied degrees and inputs.

@[simp]

theorem TauCeti.AInfinity.suspendedStasheffSum_eq_smul {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (n : ℕ) : suspendedStasheffSum m d x n = negOnePowCast R (MultilinearMap.suspExp n d) • stasheffSum m d x n

The suspended and unsuspended Stasheff identities agree up to a global sign.

theorem TauCeti.AInfinity.suspendedStasheffSum_congr {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) {e : ℕ → ℤ} {y : ℕ → A} (n : ℕ) (hd : ∀ i < n, d i = e i) (hx : ∀ i < n, x i = y i) : suspendedStasheffSum m d x n = suspendedStasheffSum m e y n

The arity-n suspended Stasheff sum only reads the first n supplied degrees and inputs.

theorem TauCeti.AInfinity.suspendedStasheffSum_eq_zero_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (n : ℕ) : suspendedStasheffSum m d x n = 0 ↔ stasheffSum m d x n = 0

The suspended Stasheff identity free of the structural coefficient holds exactly when the unsuspended one does.

theorem TauCeti.AInfinity.map_stasheffSum {R : Type uR} {A : Type uA} [CommRing R] [AddCommMonoid A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) {B : Type u_1} [AddCommMonoid B] [Module R B] (f : A →ₗ[R] B) (m' : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => B) B) (hf : ∀ (k : ℕ) (y : Fin k → A), f ((m k) y) = (m' k) fun (i : Fin k) => f (y i)) (n : ℕ) : f (stasheffSum m d x n) = stasheffSum m' d (fun (i : ℕ) => f (x i)) n

Naturality of the Stasheff sums. A linear map which intertwines two families of operations intertwines their Stasheff sums.

The identities in arities one to four

theorem TauCeti.AInfinity.stasheffSum_one {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) : stasheffSum m d x 1 = (m 1) ![(m 1) ![x 0]]

The arity-one identity is m₁ m₁ = 0.

theorem TauCeti.AInfinity.stasheffSum_two {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) : stasheffSum m d x 2 = (m 1) ![(m 2) ![x 0, x 1]] - (m 2) ![(m 1) ![x 0], x 1] - negOnePowCast R (d 0) • (m 2) ![x 0, (m 1) ![x 1]]

The arity-two identity, evaluated: m₁ m₂ - m₂ (m₁ ⊗ 1) - m₂ (1 ⊗ m₁), where the Koszul rule turns the last term into (-1) ^ (d 0) times m₂ (a, m₁ b).

theorem TauCeti.AInfinity.stasheffSum_three {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) : stasheffSum m d x 3 = (m 1) ![(m 3) ![x 0, x 1, x 2]] + (m 2) ![(m 2) ![x 0, x 1], x 2] - (m 2) ![x 0, (m 2) ![x 1, x 2]] + (m 3) ![(m 1) ![x 0], x 1, x 2] + negOnePowCast R (d 0) • (m 3) ![x 0, (m 1) ![x 1], x 2] + negOnePowCast R (d 0 + d 1) • (m 3) ![x 0, x 1, (m 1) ![x 2]]

The arity-three identity, evaluated using the supplied degrees d 0, d 1, d 2 (without a homogeneity hypothesis): m₁ m₃ + m₂ (m₂ ⊗ 1) - m₂ (1 ⊗ m₂) + m₃ (m₁ ⊗ 1 ⊗ 1 + 1 ⊗ m₁ ⊗ 1 + 1 ⊗ 1 ⊗ m₁). This display suppresses the degree-dependent Koszul factors, which are explicit in the statement.

theorem TauCeti.AInfinity.stasheffSum_four {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) : stasheffSum m d x 4 = (m 1) ![(m 4) ![x 0, x 1, x 2, x 3]] - (m 2) ![(m 3) ![x 0, x 1, x 2], x 3] - negOnePowCast R (d 0) • (m 2) ![x 0, (m 3) ![x 1, x 2, x 3]] + (m 3) ![(m 2) ![x 0, x 1], x 2, x 3] - (m 3) ![x 0, (m 2) ![x 1, x 2], x 3] + (m 3) ![x 0, x 1, (m 2) ![x 2, x 3]] - (m 4) ![(m 1) ![x 0], x 1, x 2, x 3] - negOnePowCast R (d 0) • (m 4) ![x 0, (m 1) ![x 1], x 2, x 3] - negOnePowCast R (d 0 + d 1) • (m 4) ![x 0, x 1, (m 1) ![x 2], x 3] - negOnePowCast R (d 0 + d 1 + d 2) • (m 4) ![x 0, x 1, x 2, (m 1) ![x 3]]

The arity-four identity, evaluated using the supplied degrees d 0, d 1, d 2, d 3 (without a homogeneity hypothesis): `m₁ m₄ - m₂ (m₃ ⊗ 1) - m₂ (1 ⊗ m₃) + m₃ (m₂ ⊗ 1 ⊗ 1) - m₃ (1 ⊗ m₂ ⊗ 1) + m₃ (1 ⊗ 1 ⊗ m₂)

• m₄ (m₁ ⊗ 1 ⊗ 1 ⊗ 1 + 1 ⊗ m₁ ⊗ 1 ⊗ 1 + 1 ⊗ 1 ⊗ m₁ ⊗ 1 + 1 ⊗ 1 ⊗ 1 ⊗ m₁)`. This display suppresses the degree-dependent Koszul factors, which are explicit in the statement.

theorem TauCeti.AInfinity.stasheffSum_two_eq_zero_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) : stasheffSum m d x 2 = 0 ↔ (m 1) ![(m 2) ![x 0, x 1]] = (m 2) ![(m 1) ![x 0], x 1] + negOnePowCast R (d 0) • (m 2) ![x 0, (m 1) ![x 1]]

The arity-two identity is the Leibniz rule for m₁ and m₂, with the Koszul sign (-1) ^ (d 0) on the second term.

theorem TauCeti.AInfinity.stasheffSum_three_eq_zero_iff_of_m_three_eq_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (h₃ : m 3 = 0) : stasheffSum m d x 3 = 0 ↔ (m 2) ![(m 2) ![x 0, x 1], x 2] = (m 2) ![x 0, (m 2) ![x 1, x 2]]

When m 3 vanishes, the arity-three identity is associativity of m₂.

theorem TauCeti.AInfinity.stasheffSum_four_eq_zero_of_m_three_eq_zero_of_m_four_eq_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (m : (k : ℕ) → MultilinearMap R (fun (x : Fin k) => A) A) (d : ℕ → ℤ) (x : ℕ → A) (h₃ : m 3 = 0) (h₄ : m 4 = 0) : stasheffSum m d x 4 = 0

When m 3 and m 4 vanish, the arity-four identity is vacuous.

Comparison with homogeneous inputs

theorem TauCeti.AInfinity.evalNat_mem_blockDeg {R : Type uR} {A : Type uA} [Semiring R] [AddCommMonoid A] [Module R A] {σ : Type u_1} [SetLike σ A] (𝒜 : ℤ → σ) {s : ℕ} (f : MultilinearMap R (fun (x : Fin s) => A) A) {d : ℕ → ℤ} {x : ℕ → A} (hf : MultilinearMap.IsHomogeneous f (fun (x : Fin s) => 𝒜) 𝒜 (2 - ↑s)) (p : ℕ) (hx : ∀ j < s, x (p + j) ∈ 𝒜 (d (p + j))) : (f.evalNat fun (j : ℕ) => x (p + j)) ∈ 𝒜 (blockDeg d p s)

TauCeti.AInfinity.blockDeg is the degree of the value of an operation of degree 2 - s on a block of homogeneous inputs.

theorem TauCeti.AInfinity.replaceBlock_mem_replaceDeg_of_mem_blockDeg {A : Type uA} {σ : Type u_1} [SetLike σ A] (𝒜 : ℤ → σ) {n p s : ℕ} {d : ℕ → ℤ} {x : ℕ → A} {e : A} (hx : ∀ i < n, x i ∈ 𝒜 (d i)) (he : e ∈ 𝒜 (blockDeg d p s)) (hps : p + s ≤ n) {i : ℕ} (hi : i < p + 1 + (n - p - s)) : replaceBlock x p s e i ∈ 𝒜 (replaceDeg d p s i)

The supplied degrees of a Stasheff term are the actual ones, for an arbitrary inserted element. If the inputs occurring in an arity-n word are homogeneous of degrees d and the element e replacing the block of length s at position p is homogeneous of degree blockDeg d p s, then replaceDeg records the degrees of the inputs of the outer operation. Only the inputs actually read, namely those below n, need be homogeneous.