Stasheff identities from a bar coderivation

This file identifies the Stasheff identities with the Taylor components of the square of the corresponding degree-one coderivation of the reduced tensor coalgebra. The predicate TauCeti.AInfinity.IsSuspension records the commuting suspension square on homogeneous pure tensors. If F is the resulting Taylor map and b = ReducedTensorWords.gradedCoderiv (G.shift 1) F 1, then the arity-n Taylor component of b ∘ b is exactly the suspended Stasheff sum. Consequently b ∘ b = 0 is equivalent to all unsuspended Stasheff identities.

The arities one through four are also stated explicitly. Together they pin the cohomological Getzler--Jones/Keller convention: the Leibniz sign in arity two is (-1)^|a|, arity three has ordinary associativity when the higher operations vanish, and arity four is then zero.

Main results

• TauCeti.AInfinity.IsSuspension: compatibility between a Taylor map and unsuspended operations on homogeneous tensors.
• TauCeti.AInfinity.suspensionTaylor: the Taylor map suspending a family of operations, which realizes IsSuspension for every family (TauCeti.AInfinity.isSuspension_suspensionTaylor).
• TauCeti.AInfinity.desuspension: the operations suspended by a Taylor map, of the degrees of A∞ operations when the Taylor map has degree one (TauCeti.AInfinity.isHomogeneous_desuspension).
• TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_apply: the arity component of the coderivation square is the suspended Stasheff sum.
• TauCeti.AInfinity.IsSuspension.comp_self_eq_zero_iff_forall_stasheffSum_eq_zero: a degree-one bar coderivation squares to zero exactly when all Stasheff identities hold on homogeneous inputs.
• TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_one_eq_zero_iff through taylorComponent_comp_self_four_eq_zero_iff: the vanishing criteria for the first four components, with the Stasheff identities written out verbatim.

References

• E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Sections 1--2.
• B. Keller, Introduction to A-infinity algebras and modules, Sections 3.1 and 3.6.

def TauCeti.AInfinity.IsSuspension {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (F : ReducedTensorWords R A →ₗ[R] A) (m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A) : Prop

A Taylor map F : Tᶜ(A) ⟶ A is the suspension of operations mₙ when, on every homogeneous pure tensor, it is obtained from mₙ by the Koszul sign of the tensor power of the degree--1 suspension. The grading is the unsuspended grading; the associated coderivation is built using G.shift 1.

The relation is required only on homogeneous inputs. Requiring it on arbitrary inputs with an arbitrarily supplied degree family would be inconsistent, since the suspension sign depends on those degrees.

Equations

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

theorem TauCeti.AInfinity.isSuspension_def {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (F : ReducedTensorWords R A →ₗ[R] A) (m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A) : IsSuspension G F m ↔ ∀ (n : ℕ) (hn : 0 < n) (d : ℕ → ℤ) (x : ℕ → A), (∀ i < n, x i ∈ G.piece (d i)) → F ((ReducedTensorWords.of R A ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin n) => x ↑i)) = (MultilinearMap.suspend d (m n)).evalNat x

The defining condition for a Taylor map to be the suspension of a family of operations, as a reusable Iff: this exposes the body of the predicate to consumers in other modules, for which the definition's body is not exposed.

noncomputable def TauCeti.AInfinity.suspensionTaylor {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A) : ReducedTensorWords R A →ₗ[R] A

The Taylor map suspending a family of operations. On a word of length n it evaluates m n after twisting the i-th letter by the Koszul twist of parameter n - 1 - i; on homogeneous letters these twists multiply to the suspension sign (-1) ^ suspExp n d.

Equations

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

@[simp]

theorem TauCeti.AInfinity.suspensionTaylor_of_tprod {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A) (n : { n : ℕ // 0 < n }) (x : Fin ↑n → A) : (suspensionTaylor G m) ((ReducedTensorWords.of R A n) ((PiTensorProduct.tprod R) x)) = (m ↑n) fun (i : Fin ↑n) => (G.koszulTwist (↑↑n - 1 - ↑↑i)) (x i)

The suspension Taylor map on a pure tensor word.

theorem TauCeti.AInfinity.isSuspension_suspensionTaylor {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A) : IsSuspension G (suspensionTaylor G m) m

suspensionTaylor G m is a Taylor map suspending m, so every family of operations has one.

theorem TauCeti.AInfinity.IsSuspension.taylor_eq {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F F' : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hF : IsSuspension G F m) (hF' : IsSuspension G F' m) : F = F'

Two Taylor maps which suspend the same operations are equal. Thus retaining both the suspended Taylor map and the unsuspended operations does not add unconstrained data.

theorem TauCeti.AInfinity.IsSuspension.isHomogeneous {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) (hm : ∀ (n : ℕ), 0 < n → MultilinearMap.IsHomogeneous (m n) (fun (x : Fin n) => G.piece) G.piece (2 - ↑n)) : LinearMap.IsHomogeneous F (ReducedTensorWords.gradedPiece (G.shift 1)) (G.shift 1).piece 1

A Taylor map related by suspension to operations of degree 2 - n has degree one from tensor words in the suspended grading to suspended letters. This is the homogeneity input that makes the square of its bar coderivation an ordinary coderivation.

noncomputable def TauCeti.AInfinity.desuspension {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (F : ReducedTensorWords R A →ₗ[R] A) (n : ℕ) : MultilinearMap R (fun (x : Fin n) => A) A

The desuspension of a Taylor map F : Tᶜ(sA) ⟶ sA: the operations whose suspension it is. In positive arity n it evaluates F on words of length n after twisting the i-th letter by the Koszul twist of parameter n - 1 - i, which undoes the suspension sign; in arity zero it is zero. Suspending a desuspended Taylor map recovers that Taylor map (suspensionTaylor_desuspension); conversely, operations with zero arity-zero term are recovered by desuspending any Taylor map that suspends them (IsSuspension.eq_desuspension).

Equations

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

@[simp]

theorem TauCeti.AInfinity.desuspension_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (F : ReducedTensorWords R A →ₗ[R] A) : desuspension G F 0 = 0

The desuspension of a Taylor map vanishes in arity zero.

theorem TauCeti.AInfinity.desuspension_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (F : ReducedTensorWords R A →ₗ[R] A) {n : ℕ} (hn : 0 < n) (x : Fin n → A) : (desuspension G F n) x = F ((ReducedTensorWords.of R A ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin ↑⟨n, hn⟩) => (G.koszulTwist (↑n - 1 - ↑↑i)) (x i)))

In positive arity, the desuspension evaluates the Taylor map on the word of Koszul-twisted letters.

@[simp]

theorem TauCeti.AInfinity.suspensionTaylor_desuspension {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (F : ReducedTensorWords R A →ₗ[R] A) : suspensionTaylor G (desuspension G F) = F

Suspending the desuspension of a Taylor map recovers it.

theorem TauCeti.AInfinity.isSuspension_desuspension {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A) (F : ReducedTensorWords R A →ₗ[R] A) : IsSuspension G F (desuspension G F)

Every Taylor map is the suspension of its desuspension.

theorem TauCeti.AInfinity.IsSuspension.eq_desuspension {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) (hm0 : m 0 = 0) : m = desuspension G F

Operations without an arity-zero term are the desuspension of any Taylor map suspending them; together with isSuspension_desuspension, the uncurved operations and their Taylor maps determine each other.

theorem TauCeti.AInfinity.isHomogeneous_desuspension {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} (hF : LinearMap.IsHomogeneous F (ReducedTensorWords.gradedPiece (G.shift 1)) (G.shift 1).piece 1) {n : ℕ} (hn : 0 < n) : MultilinearMap.IsHomogeneous (desuspension G F n) (fun (x : Fin n) => G.piece) G.piece (2 - ↑n)

The desuspension of a Taylor map of degree one for the suspended grading has, in each positive arity n, the degree 2 - n of an A∞ operation. This is the converse of IsSuspension.isHomogeneous.

theorem TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) {n : ℕ} (hm : ∀ (s : ℕ), 0 < s → s ≤ n → MultilinearMap.IsHomogeneous (m s) (fun (x : Fin s) => G.piece) G.piece (2 - ↑s)) (hn : 0 < n) (d : ℕ → ℤ) (x : ℕ → A) (hx : ∀ i < n, x i ∈ G.piece (d i)) : ((ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 ∘ₗ ReducedTensorWords.gradedCoderiv (G.shift 1) F 1).taylorComponent ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin n) => x ↑i) = suspendedStasheffSum m d x n

The arity-n Taylor component of the square of the suspended bar coderivation is the suspended Stasheff sum. The input elements are recorded with their unsuspended degrees d; they therefore have degrees d i - 1 for the shifted grading used by the coderivation.

theorem TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_eq_smul_stasheffSum {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) {n : ℕ} (hm : ∀ (s : ℕ), 0 < s → s ≤ n → MultilinearMap.IsHomogeneous (m s) (fun (x : Fin s) => G.piece) G.piece (2 - ↑s)) (hn : 0 < n) (d : ℕ → ℤ) (x : ℕ → A) (hx : ∀ i < n, x i ∈ G.piece (d i)) : ((ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 ∘ₗ ReducedTensorWords.gradedCoderiv (G.shift 1) F 1).taylorComponent ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin n) => x ↑i) = negOnePowCast R (MultilinearMap.suspExp n d) • stasheffSum m d x n

The arity component of the bar-coderivation square is the unsuspended Stasheff sum multiplied by the single suspension sign of the whole input tuple.

theorem TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_eq_zero_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) {n : ℕ} (hm : ∀ (s : ℕ), 0 < s → s ≤ n → MultilinearMap.IsHomogeneous (m s) (fun (x : Fin s) => G.piece) G.piece (2 - ↑s)) (hn : 0 < n) (d : ℕ → ℤ) (x : ℕ → A) (hx : ∀ i < n, x i ∈ G.piece (d i)) : ((ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 ∘ₗ ReducedTensorWords.gradedCoderiv (G.shift 1) F 1).taylorComponent ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin n) => x ↑i) = 0 ↔ stasheffSum m d x n = 0

On homogeneous inputs, an arity component of the bar-coderivation square vanishes exactly when the corresponding unsuspended Stasheff sum vanishes.

The first four components

theorem TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_one_eq_zero_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) (hm : ∀ (s : ℕ), 0 < s → s ≤ 1 → MultilinearMap.IsHomogeneous (m s) (fun (x : Fin s) => G.piece) G.piece (2 - ↑s)) (d : ℕ → ℤ) (x : ℕ → A) (hx : x 0 ∈ G.piece (d 0)) : ((ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 ∘ₗ ReducedTensorWords.gradedCoderiv (G.shift 1) F 1).taylorComponent ⟨1, taylorComponent_comp_self_one_eq_zero_iff._proof_2⟩) ((PiTensorProduct.tprod R) fun (i : Fin 1) => x ↑i) = 0 ↔ (m 1) ![(m 1) ![x 0]] = 0

The arity-one component of b ∘ b vanishes exactly when m₁ m₁ = 0.

theorem TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_two_eq_zero_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) (hm : ∀ (s : ℕ), 0 < s → s ≤ 2 → MultilinearMap.IsHomogeneous (m s) (fun (x : Fin s) => G.piece) G.piece (2 - ↑s)) (d : ℕ → ℤ) (x : ℕ → A) (hx : ∀ i < 2, x i ∈ G.piece (d i)) : ((ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 ∘ₗ ReducedTensorWords.gradedCoderiv (G.shift 1) F 1).taylorComponent ⟨2, taylorComponent_comp_self_two_eq_zero_iff._proof_2⟩) ((PiTensorProduct.tprod R) fun (i : Fin 2) => x ↑i) = 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 component of b ∘ b is zero exactly when m₁ obeys the graded Leibniz rule for m₂, with sign (-1)^(d 0) on the second differentiated input.

theorem TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_three_eq_zero_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) (hm : ∀ (s : ℕ), 0 < s → s ≤ 3 → MultilinearMap.IsHomogeneous (m s) (fun (x : Fin s) => G.piece) G.piece (2 - ↑s)) (d : ℕ → ℤ) (x : ℕ → A) (hx : ∀ i < 3, x i ∈ G.piece (d i)) : ((ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 ∘ₗ ReducedTensorWords.gradedCoderiv (G.shift 1) F 1).taylorComponent ⟨3, taylorComponent_comp_self_three_eq_zero_iff._proof_2⟩) ((PiTensorProduct.tprod R) fun (i : Fin 3) => x ↑i) = 0 ↔ (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]] = 0

The arity-three component of b ∘ b is zero exactly when the displayed arity-three Stasheff expression vanishes, including the two degree-dependent Koszul factors.

theorem TauCeti.AInfinity.IsSuspension.taylorComponent_comp_self_four_eq_zero_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) (hm : ∀ (s : ℕ), 0 < s → s ≤ 4 → MultilinearMap.IsHomogeneous (m s) (fun (x : Fin s) => G.piece) G.piece (2 - ↑s)) (d : ℕ → ℤ) (x : ℕ → A) (hx : ∀ i < 4, x i ∈ G.piece (d i)) : ((ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 ∘ₗ ReducedTensorWords.gradedCoderiv (G.shift 1) F 1).taylorComponent ⟨4, taylorComponent_comp_self_four_eq_zero_iff._proof_2⟩) ((PiTensorProduct.tprod R) fun (i : Fin 4) => x ↑i) = 0 ↔ (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]] = 0

The arity-four component of b ∘ b is zero exactly when the displayed arity-four Stasheff expression vanishes, with all four unary-insertion signs explicit.

theorem TauCeti.AInfinity.IsSuspension.comp_self_eq_zero_iff_forall_stasheffSum_eq_zero {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A} {F : ReducedTensorWords R A →ₗ[R] A} {m : (n : ℕ) → MultilinearMap R (fun (x : Fin n) => A) A} (hFm : IsSuspension G F m) (hm : ∀ (n : ℕ), 0 < n → MultilinearMap.IsHomogeneous (m n) (fun (x : Fin n) => G.piece) G.piece (2 - ↑n)) : ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 ∘ₗ ReducedTensorWords.gradedCoderiv (G.shift 1) F 1 = 0 ↔ ∀ (n : ℕ), 0 < n → ∀ (d : ℕ → ℤ) (x : ℕ → A), (∀ i < n, x i ∈ G.piece (d i)) → stasheffSum m d x n = 0

The suspended bar coderivation squares to zero exactly when the unsuspended operations obey every Stasheff identity on homogeneous inputs. Since an internal grading decomposes every element into a finite sum of homogeneous elements, testing those inputs detects the whole linear map b ∘ b, not merely its restriction to homogeneous words.