Graded coderivations of the coaugmented tensor coalgebra

TauCeti.LinearAlgebra.TensorCoalgebra.GradedCoderivation packages the q-twisted co-Leibniz rule for the reduced tensor coalgebra T = ⨁_{n ≥ 1} M^{⊗ n}. The coaugmented tensor coalgebra TauCeti.TensorWords = ⨆_{n ≥ 0} M^{⊗ n} adds the empty word, and the module and bimodule theories need b there as well, because a coderivation over b of a cofree comodule cuts a word at its two ends as well. This file provides the coaugmented counterpart: the total-letter-degree pieces, the compatibility of the letterwise maps of both presentations, and the q-twisted co-Leibniz identity of an endomorphism of tensor words.

As in the reduced case the sign is carried by the letterwise extension of the Koszul twist, which on the degree-D piece is scalar multiplication by (-1)^(q * D) and fixes the empty word, so the identity takes the sign-free shape

Δ ∘ b = (b ⊗ 1) ∘ Δ + (1 ⊗ b) ∘ (τ ⊗ 1) ∘ Δ

in which τ = TensorWords.map (InternalGrading.koszulTwist G q) acts on the left half of every cut; the letterwise maps themselves are in TauCeti.LinearAlgebra.TensorCoalgebra.Coaugmented.Basic, which also shows that this τ restricts to the reduced twist on the words of positive length. Homogeneity of b in the total letter degree is a separate condition, recorded by TauCeti.TensorWords.gradedPiece; the predicate TensorWords.IsGradedCoderivation G q is the q-twisted co-Leibniz condition alone, and it depends only on the parity of q.

Main definitions

• TauCeti.TensorWords.gradedPiece: the words whose letters have total degree D.
• TauCeti.TensorWords.IsGradedCoderivation: the q-twisted co-Leibniz identity of an endomorphism of tensor words.

Main results

• TauCeti.TensorWords.iSup_gradedPiece_eq_top: the total-degree pieces span the coaugmented tensor coalgebra, so an identity of linear maps out of tensor words may be checked piecewise.
• TauCeti.TensorWords.mem_gradedPiece_of_reducedInclusion: the total-degree pieces of the reduced tensor coalgebra embed into the coaugmented ones.
• TauCeti.TensorWords.map_koszulTwist_apply_of_mem: on the degree-D piece the letterwise Koszul twist is scalar multiplication by (-1) ^ (q * D).

Getzler--Jones, Sections 1--2, and Keller, Section 3.6, supply the suspended bar convention these identities encode.

The grading by total letter degree

noncomputable def TauCeti.TensorWords.gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (D : ℤ) : Submodule R (TensorWords R M)

The words of total degree D: the span of the pure tensor words whose letters lie in homogeneous pieces the degrees of which add up to D.

Equations

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

theorem TauCeti.TensorWords.gradedPiece_induction {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M} {D : ℤ} {motive : TensorWords R M → Prop} {z : TensorWords R M} (hz : z ∈ gradedPiece G D) (mem : ∀ (n : ℕ) (𝒟 : Fin n → ℤ) (x : Fin n → M), (∀ (i : Fin n), x i ∈ G.piece (𝒟 i)) → ∑ i : Fin n, 𝒟 i = D → motive ((of R M n) ((PiTensorProduct.tprod R) x))) (zero : motive 0) (add : ∀ (u v : TensorWords R M), u ∈ gradedPiece G D → v ∈ gradedPiece G D → motive u → motive v → motive (u + v)) (smul : ∀ (a : R), ∀ u ∈ gradedPiece G D, motive u → motive (a • u)) : motive z

Induction on membership in gradedPiece: a consumer may apply this in place of Submodule.span_induction, whose span is sealed behind the definition.

theorem TauCeti.TensorWords.mem_gradedPiece_of_tprod {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) {n : ℕ} (x : Fin n → M) (𝒟 : Fin n → ℤ) (h𝒟 : ∀ (i : Fin n), x i ∈ G.piece (𝒟 i)) : (of R M n) ((PiTensorProduct.tprod R) x) ∈ gradedPiece G (∑ i : Fin n, 𝒟 i)

A pure tensor word of homogeneous letters of degrees 𝒟 i lies in the graded piece of total degree ∑ i, 𝒟 i.

theorem TauCeti.TensorWords.iSup_gradedPiece_eq_top {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : ⨆ (D : ℤ), gradedPiece G D = ⊤

The total-degree pieces span the coaugmented tensor words. In particular, an equality of linear maps out of tensor words may be checked separately on these pieces.

theorem TauCeti.TensorWords.map_koszulTwist_apply_of_mem {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) {D : ℤ} {z : TensorWords R M} (hz : z ∈ gradedPiece G D) (q : ℤ) : (map (G.koszulTwist q)) z = ↑↑(q * D).negOnePow • z

On the total-degree-D piece of tensor words, applying the Koszul twist to every letter is scalar multiplication by (-1) ^ (q * D).

theorem TauCeti.TensorWords.mem_gradedPiece_of_reducedInclusion {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M} {D : ℤ} {w : ReducedTensorWords R M} (hw : w ∈ ReducedTensorWords.gradedPiece G D) : (reducedInclusion R M) w ∈ gradedPiece G D

A word of the reduced tensor coalgebra is a coaugmented word of the same total degree, so the reduced degree pieces embed into the coaugmented ones.

The q-twisted co-Leibniz identity

def TauCeti.TensorWords.IsGradedCoderivation {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) (q : ℤ) (b : TensorWords R M →ₗ[R] TensorWords R M) : Prop

A q-twisted co-Leibniz condition on an endomorphism b of the coaugmented tensor coalgebra: the co-Leibniz rule with the Koszul sign of the left cut half,

Δ ∘ b = (b ⊗ 1) ∘ Δ + (1 ⊗ b) ∘ (τ ⊗ 1) ∘ Δ,

in which τ = TensorWords.map (InternalGrading.koszulTwist G q) is the letterwise extension of the Koszul twist and acts on the left half of every cut, exactly as in TauCeti.ReducedTensorWords.IsGradedCoderivation. This is only the twisted co-Leibniz condition, not a homogeneity requirement on b; degree-q homogeneity in the total letter degree is separate and is recorded by TauCeti.TensorWords.gradedPiece. Nor does the condition itself require b to annihilate the empty word: the extensions by zero on the empty word of reduced coderivations, such as TauCeti.AInfinityAlgebra.coaugmentedBarDifferential, satisfy it, by TauCeti.TensorWords.isGradedCoderivation_extendReduced.

Equations

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

theorem TauCeti.TensorWords.isGradedCoderivation_iff {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M} {q : ℤ} {b : TensorWords R M →ₗ[R] TensorWords R M} : IsGradedCoderivation G q b ↔ deconcatenation R M ∘ₗ b = LinearMap.rTensor (TensorWords R M) b ∘ₗ deconcatenation R M + (LinearMap.lTensor (TensorWords R M) b ∘ₗ LinearMap.rTensor (TensorWords R M) (map (G.koszulTwist q))) ∘ₗ deconcatenation R M

The co-Leibniz identity of a graded coderivation, 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.

theorem TauCeti.TensorWords.IsGradedCoderivation.deconcatenation_apply {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M} {q : ℤ} {b : TensorWords R M →ₗ[R] TensorWords R M} (hb : IsGradedCoderivation G q b) (z : TensorWords R M) : (deconcatenation R M) (b z) = (LinearMap.rTensor (TensorWords R M) b) ((deconcatenation R M) z) + (LinearMap.lTensor (TensorWords R M) b) ((LinearMap.rTensor (TensorWords R M) (map (G.koszulTwist q))) ((deconcatenation R M) z))

The co-Leibniz identity of a graded coderivation, applied to an element.