Graded coderivations of the reduced tensor coalgebra

Let M carry an internal integer grading G, and let T = ⨁_{n ≥ 1} M^{⊗ n} be the reduced tensor coalgebra of TauCeti.ReducedTensorWords. The ungraded correspondence of TauCeti.ReducedTensorWords.coderivEquivTaylor matches coderivations with their Taylor components, but an operation of degree q assembles into a q-twisted coderivation: it satisfies the co-Leibniz rule with a Koszul sign, cutting its value giving the cut halves with b applied to one half, scaled by the sign (-1)^(q * |w₁|) when b is applied to the right half w₂. This file packages that signed correspondence. Homogeneity of degree q is separate, and is recorded by isHomogeneous_gradedCoderiv.

The sign is not carried by hand. The Koszul twist TauCeti.InternalGrading.koszulTwist G q scales each homogeneous element of degree e by (-1)^(q * e), and the letterwise extension ReducedTensorWords.map lifts it to words. Precomposing each Taylor summand with the twist of the letters preceding its collapsed block produces exactly the signs (-1)^(q * (|x₀| + ⋯ + |x_{p - 1}|)) of the classical suspended formula (0-based positions; p is the number of letters preceding the collapsed block), and the twisted co-Leibniz identity takes the sign-free shape

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

in which τ = ReducedTensorWords.map (InternalGrading.koszulTwist G q) acts on the left half of every cut. For q = 0 this reduces term by term to the ungraded theory: the twist of parameter zero is the identity, so a 0-twisted graded coderivation is exactly an ungraded coderivation. The predicate IsGradedCoderivation G q is this q-twisted co-Leibniz condition; it does not include homogeneity of b, and it depends only on the parity of q. Homogeneity is recorded separately by isHomogeneous_gradedCoderiv and IsGradedCoderivation.isHomogeneous.

Main definitions

• TauCeti.ReducedTensorWords.gradedCoderiv: the graded Taylor expansion of a linear map F from words to letters, at twist parameter q.
• TauCeti.ReducedTensorWords.IsGradedCoderivation: the q-twisted co-Leibniz identity of an endomorphism of words.
• TauCeti.ReducedTensorWords.gradedPiece: the words whose letters have total degree D.
• TauCeti.ReducedTensorWords.gradedCoderivations: the submodule of q-twisted coderivations.

Main results

• TauCeti.ReducedTensorWords.isGradedCoderivation_gradedCoderiv, TauCeti.ReducedTensorWords.letter_comp_gradedCoderiv: gradedCoderiv G F q is a q-twisted coderivation with letter component F.
• TauCeti.ReducedTensorWords.IsGradedCoderivation.eq_of_letter_comp_eq: a graded coderivation is determined by its letter component.
• TauCeti.ReducedTensorWords.gradedCoderiv_comp_letter_of_tprod: the coderivation extending a map of letters applies it to one letter at a time, twisting the letters before it.
• TauCeti.ReducedTensorWords.iSup_gradedPiece_eq_top: the total-degree pieces span the reduced tensor coalgebra.
• TauCeti.ReducedTensorWords.prepend_mem_gradedPiece, TauCeti.ReducedTensorWords.subword_mem_gradedPiece: prepending a homogeneous letter and taking a block of homogeneous letters have the expected total degrees.
• TauCeti.ReducedTensorWords.isHomogeneous_map: applying a degree-zero homogeneous map to every letter preserves the total degree of a word.
• TauCeti.ReducedTensorWords.map_koszulTwist_apply_of_mem: the letterwise twist has the expected scalar action on each total-degree piece.
• TauCeti.LinearMap.IsHomogeneous.map_koszulTwist_comp: a homogeneous linear map of reduced tensor words commutes with the letterwise twist up to the sign given by its degree.
• TauCeti.ReducedTensorWords.IsGradedCoderivation.isCoderivation_comp_self: a graded coderivation anticommuting with its letterwise Koszul twist has an ordinary coderivation as its square.
• TauCeti.ReducedTensorWords.isHomogeneous_gradedCoderiv: if F raises degrees by r then so does gradedCoderiv G F q, independently of the twist parameter.
• TauCeti.ReducedTensorWords.gradedCoderivEquivTaylor: the q-twisted coderivations form a submodule identified, through the letter components, with the maps from tensor words to letters.

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.

noncomputable def TauCeti.ReducedTensorWords.gradedCoderiv {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M

The graded Taylor expansion of a map F from words to single letters, at twist parameter q: on a tensor word it collapses each block to the letter that F produces from it, composed with the twist of the letters preceding the block.

If the inputs are homogeneous of degrees 𝒟 i, the collapse at position p thus carries the Koszul sign (-1)^(q * (𝒟 0 + ⋯ + 𝒟 (p - 1))), because the Koszul twist scales each of those letters by its own sign factor; see gradedCoderiv_of_tprod_of_homogeneous.

Equations

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

theorem TauCeti.ReducedTensorWords.gradedCoderiv_of_tprod {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) {n : ℕ} (hn : 0 < n) (x : Fin n → M) : (gradedCoderiv G F q) ((of R M ⟨n, hn⟩) ((PiTensorProduct.tprod R) x)) = ∑ p ∈ Finset.range n, ∑ d ∈ Finset.range (n + 1), splice R (G.twistedTuple q x 0 p) 0 n p d (F (subword R x p d))

Evaluation of the graded Taylor expansion on a pure tensor word: every summand collapses one block and twists the letters preceding it.

theorem TauCeti.ReducedTensorWords.splice_twistedTuple_smul {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) {n : ℕ} (x : Fin n → M) (𝒟 : Fin n → ℤ) (hx : ∀ (i : Fin n), x i ∈ G.piece (𝒟 i)) (p d : ℕ) (e : M) : splice R (G.twistedTuple q x 0 p) 0 n p d e = ↑↑(q * ∑ j ∈ Finset.range p, if h : j < n then 𝒟 ⟨j, h⟩ else 0).negOnePow • splice R x 0 n p d e

Splicing a Koszul-twisted prefix of a homogeneous tuple produces the Koszul sign of that prefix times the untwisted splice.

theorem TauCeti.ReducedTensorWords.gradedCoderiv_of_tprod_of_homogeneous {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) {n : ℕ} (hn : 0 < n) (x : Fin n → M) (𝒟 : Fin n → ℤ) (hx : ∀ (i : Fin n), x i ∈ G.piece (𝒟 i)) : (gradedCoderiv G F q) ((of R M ⟨n, hn⟩) ((PiTensorProduct.tprod R) x)) = ∑ p ∈ Finset.range n, ∑ d ∈ Finset.range (n + 1), ↑↑(q * ∑ j ∈ Finset.range p, if h : j < n then 𝒟 ⟨j, h⟩ else 0).negOnePow • splice R x 0 n p d (F (subword R x p d))

Evaluation of the graded Taylor expansion on a pure tensor of homogeneous letters: each summand is the corresponding untwisted splice, scaled by the Koszul sign (-1)^(q * (𝒟 0 + ⋯ + 𝒟 (p - 1))) of the letters preceding the collapsed block.

theorem TauCeti.ReducedTensorWords.gradedCoderiv_comp_letter_of_tprod {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (f : M →ₗ[R] M) (q : ℤ) {n : ℕ} (hn : 0 < n) (x : Fin n → M) : (gradedCoderiv G (f ∘ₗ letter R M) q) ((of R M ⟨n, hn⟩) ((PiTensorProduct.tprod R) x)) = ∑ p ∈ Finset.range n, (of R M ⟨n, hn⟩) ((PiTensorProduct.tprod R) fun (i : Fin ↑⟨n, hn⟩) => if ↑i < p then (G.koszulTwist q) (x i) else if ↑i = p then f (x i) else x i)

Evaluation of the graded Taylor expansion of a map acting on single letters only: it applies f to one letter at a time and twists the letters preceding it. On homogeneous letters the twist is the Koszul sign of moving an operation of degree q past those letters.

theorem TauCeti.ReducedTensorWords.gradedCoderiv_subword {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) {n : ℕ} (x : Fin n → M) {a b K : ℕ} (hK : b ≤ K) : (gradedCoderiv G F q) (subword R x a b) = ∑ p ∈ Finset.range K, ∑ d ∈ Finset.range (K + 1), splice R (G.twistedTuple q x a p) a b p d (F (subword R x (a + p) d))

Evaluation of the graded Taylor expansion on a block of a pure tensor word: the same sums as for the ungraded coderiv_subword, with each spliced tuple twisted before the block that collapses. The two ranges may be taken as large as convenient, since a summand whose collapsed block does not fit vanishes.

The grading by total letter degree

noncomputable def TauCeti.ReducedTensorWords.gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (D : ℤ) : Submodule R (ReducedTensorWords 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.ReducedTensorWords.gradedPiece_induction {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {D : ℤ} {motive : ReducedTensorWords R M → Prop} {z : ReducedTensorWords R M} (hz : z ∈ gradedPiece G D) (mem : ∀ (n : ℕ) (hn : 0 < 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, hn⟩) ((PiTensorProduct.tprod R) x))) (zero : motive 0) (add : ∀ (u v : ReducedTensorWords 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.ReducedTensorWords.mem_gradedPiece_of_tprod {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {n : ℕ} (hn : 0 < n) (x : Fin n → M) (𝒟 : Fin n → ℤ) (h𝒟 : ∀ (i : Fin n), x i ∈ G.piece (𝒟 i)) : (of R M ⟨n, hn⟩) ((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.ReducedTensorWords.ofLetter_mem_gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {p : ℤ} {x : M} (hx : x ∈ G.piece p) : (ofLetter R M) x ∈ gradedPiece G p

A single homogeneous letter is a word of the same total degree.

theorem TauCeti.ReducedTensorWords.prepend_mem_gradedPiece {R : Type uR} [CommRing R] {N : Type uN} [AddCommMonoid N] [Module R N] {H : InternalGrading R N} {p D : ℤ} {a : N} (ha : a ∈ H.piece p) {w : ReducedTensorWords R N} (hw : w ∈ gradedPiece H D) : ((prepend R N) a) w ∈ gradedPiece H (p + D)

Prepending a letter of degree p to a word of total degree D gives a word of total degree p + D.

theorem TauCeti.ReducedTensorWords.subword_mem_gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {n : ℕ} (x : Fin n → M) (𝒟 : ℕ → ℤ) (h𝒟 : ∀ (i : Fin n), x i ∈ G.piece (𝒟 ↑i)) (a b : ℕ) (hab : a + b ≤ n) : subword R x a b ∈ gradedPiece G (∑ j ∈ Finset.range b, 𝒟 (a + j))

A block of a pure tensor word of homogeneous letters lies in the graded piece of the sum of the degrees of its letters. The degree family is indexed by absolute positions.

theorem TauCeti.ReducedTensorWords.isHomogeneous_letter {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) : LinearMap.IsHomogeneous (letter R M) (gradedPiece G) G.piece 0

Projecting a word onto its length-one component preserves the total degree.

theorem TauCeti.ReducedTensorWords.isHomogeneous_map {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] (G : InternalGrading R M) (H : InternalGrading R N) {f : M →ₗ[R] N} (hf : LinearMap.IsHomogeneous f G.piece H.piece 0) : LinearMap.IsHomogeneous (map R f) (gradedPiece G) (gradedPiece H) 0

Applying a degree-zero homogeneous map to every letter preserves the total degree of a word: the letterwise extension ReducedTensorWords.map f is homogeneous of degree zero for the total degree gradings.

theorem TauCeti.ReducedTensorWords.splice_mem_gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {n : ℕ} (x : Fin n → M) (𝒟 : ℕ → ℤ) (h𝒟 : ∀ (i : Fin n), x i ∈ G.piece (𝒟 ↑i)) (p d : ℕ) {E : ℤ} {e : M} (he : e ∈ G.piece E) (hpd : p + d ≤ n) : splice R x 0 n p d e ∈ gradedPiece G (∑ j ∈ Finset.range p, 𝒟 j + E + ∑ j ∈ Finset.range (n - p - d), 𝒟 (p + d + j))

Splicing one homogeneous letter into a word of homogeneous letters stays inside the graded piece: the total degree is that of the untouched prefix and suffix plus the degree of the new letter. The degree family is indexed by absolute positions, since splicing shifts them.

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

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

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

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

theorem TauCeti.LinearMap.IsHomogeneous.map_koszulTwist_comp {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] {G : InternalGrading R M} {H : InternalGrading R N} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R N} {r : ℤ} (hb : IsHomogeneous b (ReducedTensorWords.gradedPiece G) (ReducedTensorWords.gradedPiece H) r) (q : ℤ) : ReducedTensorWords.map R (H.koszulTwist q) ∘ₗ b = ↑↑(q * r).negOnePow • b ∘ₗ ReducedTensorWords.map R (G.koszulTwist q)

A homogeneous linear map of reduced tensor words commutes with the letterwise Koszul twists up to the sign contributed by its degree.

theorem TauCeti.ReducedTensorWords.isHomogeneous_gradedCoderiv {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) (q r : ℤ) (hF : LinearMap.IsHomogeneous F (gradedPiece G) (fun (e : ℤ) => G.piece e) r) : LinearMap.IsHomogeneous (gradedCoderiv G F q) (gradedPiece G) (gradedPiece G) r

If F raises total degrees by r, so does its graded Taylor expansion, independently of the twist parameter q: for every D, the map gradedCoderiv G F q sends gradedPiece G D into gradedPiece G (D + r). The twist preserves each homogeneous piece.

Graded coderivations

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

A graded coderivation of twist parameter q of the reduced tensor coalgebra: an endomorphism b satisfying the co-Leibniz rule with the Koszul sign of the left cut half,

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

in which τ = ReducedTensorWords.map (InternalGrading.koszulTwist G q) is the letterwise extension of the Koszul twist and acts on the left half of every cut. This is only the twisted co-Leibniz condition, not a homogeneity requirement on b; it depends only on the parity of q. On a word z of homogeneous letters, summing over cuts w₁ ⊗ w₂ of z,

Δ (b z) = ∑ (b w₁ ⊗ w₂ + (-1)^(q * |w₁|) • (w₁ ⊗ b w₂)),

the classical signed co-Leibniz rule. For q = 0 the twist is the identity and this is plain IsCoderivation. Homogeneity of degree r is recorded by IsGradedCoderivation.isHomogeneous.

Equations

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

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

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

theorem TauCeti.ReducedTensorWords.isGradedCoderivation_iff {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {q : ℤ} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} : IsGradedCoderivation G q b ↔ deconcatenation R M ∘ₗ b = LinearMap.rTensor (ReducedTensorWords R M) b ∘ₗ deconcatenation R M + (LinearMap.lTensor (ReducedTensorWords R M) b ∘ₗ LinearMap.rTensor (ReducedTensorWords R M) (map R (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.ReducedTensorWords.IsGradedCoderivation.eq_of_letter_comp_eq {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {q : ℤ} {b₁ b₂ : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (h₁ : IsGradedCoderivation G q b₁) (h₂ : IsGradedCoderivation G q b₂) (hl : letter R M ∘ₗ b₁ = letter R M ∘ₗ b₂) : b₁ = b₂

A q-twisted graded coderivation of the reduced tensor coalgebra is determined by its letter component, that is by its composite with the projection onto single letters: two such coderivations whose letter components agree are equal. This is the signed analogue of TauCeti.ReducedTensorWords.IsCoderivation.eq_of_letter_comp_eq.

@[simp]

theorem TauCeti.ReducedTensorWords.isGradedCoderivation_gradedCoderiv {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : IsGradedCoderivation G q (gradedCoderiv G F q)

The graded Taylor expansion of any linear map F from tensor words to letters is a q-twisted coderivation: the signed analogue of isCoderivation_coderiv. The twist of the letters preceding each collapsed block produces exactly the Koszul sign (-1)^(q * |left half|) of the co-Leibniz rule, so the identity holds for an arbitrary F, homogeneous or not.

Determinedness and the correspondence

@[simp]

theorem TauCeti.ReducedTensorWords.letter_comp_gradedCoderiv {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) : letter R M ∘ₗ gradedCoderiv G F q = F

The Taylor components of the graded Taylor expansion are the given map: the only summand leaving a single letter is the one collapsing the whole word, whose preceding twist is empty.

@[simp]

theorem TauCeti.ReducedTensorWords.taylorComponent_gradedCoderiv {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) (q : ℤ) (n : { n : ℕ // 0 < n }) : (gradedCoderiv G F q).taylorComponent n = F ∘ₗ of R M n

The arity-n component of a graded Taylor expansion is the restriction of its defining Taylor map to words of length n.

theorem TauCeti.ReducedTensorWords.IsGradedCoderivation.isHomogeneous {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {q r : ℤ} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hb : IsGradedCoderivation G q b) (hhom : LinearMap.IsHomogeneous (letter R M ∘ₗ b) (gradedPiece G) (fun (e : ℤ) => G.piece e) r) : LinearMap.IsHomogeneous b (gradedPiece G) (gradedPiece G) r

A graded coderivation whose letter component raises degrees by r raises degrees by r: being determined by its letter component, it inherits homogeneity from it. The twist parameter q of the co-Leibniz identity is independent of this shift.

Squares of anticommuting graded coderivations

theorem TauCeti.ReducedTensorWords.IsGradedCoderivation.isCoderivation_comp_self {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] {G : InternalGrading R M} {q : ℤ} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hb : IsGradedCoderivation G q b) (hodd : b ∘ₗ map R (G.koszulTwist q) + map R (G.koszulTwist q) ∘ₗ b = 0) : IsCoderivation R (b ∘ₗ b)

The square of a graded coderivation anticommuting with the letterwise Koszul twist is an ordinary coderivation. The anticommutation relation expresses oddness when q is odd. For even q, the twist is the identity and the hypothesis instead reduces to b + b = 0.

Twist parameter zero

theorem TauCeti.ReducedTensorWords.IsGradedCoderivation.isCoderivation {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 0 b) : IsCoderivation R b

A 0-twisted graded coderivation is a coderivation: the twist of parameter zero is the identity, so the Koszul sign drops out of the co-Leibniz rule.

theorem TauCeti.ReducedTensorWords.IsCoderivation.isGradedCoderivation {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 : IsCoderivation R b) : IsGradedCoderivation G 0 b

A coderivation is a 0-twisted graded coderivation.

@[simp]

theorem TauCeti.ReducedTensorWords.gradedCoderiv_zero {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (F : ReducedTensorWords R M →ₗ[R] M) : gradedCoderiv G F 0 = coderiv R F

At twist parameter zero the graded Taylor expansion is the ungraded one.

The submodule of graded coderivations

noncomputable def TauCeti.ReducedTensorWords.gradedCoderivations {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) : Submodule R (ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M)

The q-twisted coderivations of the reduced tensor coalgebra form an R-submodule of its endomorphisms: both sides of the twisted co-Leibniz identity depend linearly on the endomorphism b. Membership is the co-Leibniz condition only; it does not include homogeneity, and it depends only on the parity of q. See isHomogeneous_gradedCoderiv and IsGradedCoderivation.isHomogeneous for the degree statement.

Equations

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

@[simp]

theorem TauCeti.ReducedTensorWords.mem_gradedCoderivations {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) {q : ℤ} {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} : b ∈ gradedCoderivations G q ↔ IsGradedCoderivation G q b

Membership in gradedCoderivations is, by definition, being a graded coderivation.

noncomputable def TauCeti.ReducedTensorWords.gradedCoderivEquivTaylor {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) : ↥(gradedCoderivations G q) ≃ₗ[R] ReducedTensorWords R M →ₗ[R] M

The graded coderivation/Taylor correspondence: a q-twisted coderivation (the co-Leibniz condition, not a homogeneity hypothesis) is determined by its letter component, and every linear map from tensor words to letters is the letter component of exactly one such coderivation, namely its graded Taylor expansion gradedCoderiv G F q. The carrier depends only on the parity of q. This is the signed analogue of ReducedTensorWords.coderivEquivTaylor.

Equations

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

@[simp]

theorem TauCeti.ReducedTensorWords.gradedCoderivEquivTaylor_apply {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) (b : ↥(gradedCoderivations G q)) : (gradedCoderivEquivTaylor G q) b = letter R M ∘ₗ ↑b

The graded coderivation/Taylor equivalence sends a coderivation to its letter component.

@[simp]

theorem TauCeti.ReducedTensorWords.gradedCoderivEquivTaylor_symm_apply {R : Type uR} {M : Type uM} [CommRing R] [AddCommMonoid M] [Module R M] (G : InternalGrading R M) (q : ℤ) (F : ReducedTensorWords R M →ₗ[R] M) : (gradedCoderivEquivTaylor G q).symm F = ⟨gradedCoderiv G F q, ⋯⟩

The inverse of the graded coderivation/Taylor equivalence is the graded Taylor expansion.