Odd squares of homogeneous tensor-coalgebra coderivations

A homogeneous endomorphism of the reduced tensor coalgebra whose degree r and twist parameter q satisfy (-1)^(q * r) = -1 is odd: it anticommutes with the letterwise Koszul involution of parameter q. Consequently the square of such a graded coderivation is an ordinary coderivation, whose vanishing can then be checked with the existing Taylor-component criterion. The degree-one case q = r = 1 is the one the A∞ sign audit consumes.

Homogeneity is genuinely needed: TauCeti.ReducedTensorWords.IsGradedCoderivation G q is the q-twisted co-Leibniz identity alone and does not by itself constrain degrees. The oddness comes from TauCeti.LinearMap.IsHomogeneous.map_koszulTwist_comp, which turns the usual calculation on a homogeneous word into an equality of endomorphisms.

Main results

• TauCeti.LinearMap.IsHomogeneous.anticommute_map_koszulTwist: a homogeneous endomorphism of reduced tensor words anticommutes with the letterwise Koszul involution as soon as the sign (-1)^(q * r) of its degree against the twist parameter is -1.
• TauCeti.LinearMap.IsHomogeneous.anticommute_map_koszulTwist_one: the degree-one case, at twist parameter one.
• TauCeti.ReducedTensorWords.IsGradedCoderivation.isCoderivation_comp_self_of_isHomogeneous: the square of such a homogeneous graded coderivation is an ordinary coderivation.
• TauCeti.ReducedTensorWords.IsGradedCoderivation.isCoderivation_comp_self_of_isHomogeneous_one: the degree-one case, at twist parameter one.

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.

theorem TauCeti.LinearMap.IsHomogeneous.anticommute_map_koszulTwist {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} {q r : ℤ} (hb : IsHomogeneous b (ReducedTensorWords.gradedPiece G) (ReducedTensorWords.gradedPiece G) r) (hqr : ↑↑(q * r).negOnePow = -1) : b ∘ₗ ReducedTensorWords.map R (G.koszulTwist q) + ReducedTensorWords.map R (G.koszulTwist q) ∘ₗ b = 0

A homogeneous endomorphism of degree r anticommutes with the letterwise Koszul twist of parameter q, provided the sign (-1)^(q * r) it commutes past that twist with is -1.

theorem TauCeti.LinearMap.IsHomogeneous.anticommute_map_koszulTwist_one {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hb : IsHomogeneous b (ReducedTensorWords.gradedPiece G) (ReducedTensorWords.gradedPiece G) 1) : b ∘ₗ ReducedTensorWords.map R (G.koszulTwist 1) + ReducedTensorWords.map R (G.koszulTwist 1) ∘ₗ b = 0

A homogeneous endomorphism of degree one anticommutes with the letterwise Koszul twist of parameter one.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivation.isCoderivation_comp_self_of_isHomogeneous {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} {q r : ℤ} (hb : IsGradedCoderivation G q b) (hhom : LinearMap.IsHomogeneous b (gradedPiece G) (gradedPiece G) r) (hqr : ↑↑(q * r).negOnePow = -1) : IsCoderivation R (b ∘ₗ b)

The square of a homogeneous graded coderivation is an ordinary coderivation as soon as the sign (-1)^(q * r) of its degree r against the twist parameter q is -1: homogeneity then supplies the anticommutation with the Koszul twist that cancels the two mixed terms in the co-Leibniz expansion. A caller holding homogeneity of the letter component instead obtains hhom from TauCeti.ReducedTensorWords.IsGradedCoderivation.isHomogeneous.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivation.isCoderivation_comp_self_of_isHomogeneous_one {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hb : IsGradedCoderivation G 1 b) (hhom : LinearMap.IsHomogeneous b (gradedPiece G) (gradedPiece G) 1) : IsCoderivation R (b ∘ₗ b)

The square of a homogeneous degree-one graded coderivation is an ordinary coderivation.