Coderivations of the reduced tensor coalgebra

For an R-module M, the reduced tensor words ⨁_{n ≥ 1} M^{⊗n} carry the reduced deconcatenation coproduct Δ built in TauCeti.ReducedTensorWords.deconcatenation. A coderivation is a linear endomorphism b satisfying the co-Leibniz rule Δ ∘ b = (b ⊗ 1 + 1 ⊗ b) ∘ Δ. This file proves that coderivations are exactly their Taylor components: composing with the projection letter onto single letters is a linear isomorphism from the coderivations onto the linear maps ⨁_{n ≥ 1} M^{⊗n} ⟶ M.

That coderivations are determined by their Taylor components is an induction along the conilpotence filtration: a word of length at most n + 1 is cut into two words of length at most n, so the right-hand side of the co-Leibniz rule is already known by induction, and a tensor word is determined by its cut together with its letter. That every family of components occurs is the explicit Taylor expansion coderiv, which collapses each nonempty block of letters of a word to the single letter the components produce from that block. Verifying its co-Leibniz rule is a reindexing: on both sides the summands are indexed by a cut position together with a collapsed block, and a cut never splits a block nor the letter that replaced one.

This is the encoding in which an A∞ algebra is a square-zero coderivation of the bar coalgebra of a suspended graded module, and its Taylor components are the operations m_n; that use is downstream, in the DGAInfinity roadmap.

Main definitions

• TauCeti.ReducedTensorWords.IsCoderivation: the co-Leibniz rule.
• TauCeti.ReducedTensorWords.coderiv: the coderivation with prescribed Taylor components.
• TauCeti.ReducedTensorWords.coderivations: the submodule of coderivations.
• LinearMap.taylorComponent: the arity component of a linear endomorphism of reduced tensor words.

Main results

• TauCeti.ReducedTensorWords.IsCoderivation.eq_of_letter_comp_eq: a coderivation is determined by its Taylor components.
• TauCeti.ReducedTensorWords.isCoderivation_coderiv and TauCeti.ReducedTensorWords.letter_comp_coderiv: coderiv F is a coderivation with Taylor components F.
• TauCeti.ReducedTensorWords.coderivEquivTaylor: coderivations are linearly isomorphic to their Taylor components.
• TauCeti.ReducedTensorWords.IsCoderivation.eq_zero_iff_taylorComponent_eq_zero: a coderivation vanishes exactly when all of its arity components vanish.

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.coderivSummand (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) (n p d : ℕ) : TensorPower R n M →ₗ[R] ReducedTensorWords R M

The (p, d) summand of the Taylor expansion of a coderivation with components F, on tensor words of length n: collapse the d letters at position p to the single letter that F produces from them.

It is zero unless the collapsed block is nonempty and fits, that is unless 0 < d and p + d ≤ n.

This is an implementation device for the coderivation/Taylor correspondence, kept public because the graded, signed correspondence in TauCeti.LinearAlgebra.TensorCoalgebra.GradedCoderivation precomposes it with a twist of the letters preceding the collapsed block.

Equations

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

theorem TauCeti.ReducedTensorWords.coderivSummand_eq_zero (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) {n p d : ℕ} (h : ¬(0 < d ∧ p + d ≤ n)) : coderivSummand R F n p d = 0

Outside its range a Taylor summand vanishes.

theorem TauCeti.ReducedTensorWords.coderivSummand_tprod (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) {n p d : ℕ} (hd : 0 < d) (hpd : p + d ≤ n) (x : Fin n → M) : (coderivSummand R F n p d) ((PiTensorProduct.tprod R) x) = splice R x 0 n p d (F (subword R x p d))

On a pure tensor word, a Taylor summand is the splice of the value of F on the collapsed block.

noncomputable def TauCeti.ReducedTensorWords.coderiv (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M

The linear endomorphism of the reduced tensor coalgebra whose Taylor components are F: on a tensor word it collapses each nonempty block of letters to the single letter that F produces from that block, and sums over all blocks.

Equations

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

theorem TauCeti.ReducedTensorWords.coderivSummand_tprod_of_eq (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) {n b : ℕ} (x : Fin n → M) (y : Fin b → M) {a : ℕ} (hab : a + b ≤ n) (hy : ∀ (j : ℕ) (hj : j < b), y ⟨j, hj⟩ = x ⟨a + j, ⋯⟩) (p d : ℕ) : (coderivSummand R F b p d) ((PiTensorProduct.tprod R) y) = splice R x a b p d (F (subword R x (a + p) d))

A Taylor summand on a tensor word that is a block of a longer tuple, read back in that tuple.

theorem TauCeti.ReducedTensorWords.coderiv_subword (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) {n : ℕ} (x : Fin n → M) {a b K : ℕ} (hK : b ≤ K) : (coderiv R F) (subword R x a b) = ∑ p ∈ Finset.range K, ∑ d ∈ Finset.range (K + 1), splice R x a b p d (F (subword R x (a + p) d))

The Taylor expansion of coderiv F on a block of a tensor word. The two ranges may be taken as large as convenient, since a summand whose collapsed block does not fit inside the block vanishes; that is what lets the expansions of a word and of its two halves be summed over one common range.

def TauCeti.ReducedTensorWords.IsCoderivation (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M) : Prop

A linear endomorphism of the reduced tensor coalgebra is a coderivation when it satisfies the co-Leibniz rule: cutting its value is the same as cutting first and applying it to one of the two halves.

Equations

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

theorem TauCeti.ReducedTensorWords.IsCoderivation.deconcatenation_apply {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hb : IsCoderivation R 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) ((deconcatenation R M) z)

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

theorem TauCeti.ReducedTensorWords.isCoderivation_iff {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} : IsCoderivation R b ↔ deconcatenation R M ∘ₗ b = (LinearMap.rTensor (ReducedTensorWords R M) b + LinearMap.lTensor (ReducedTensorWords R M) b) ∘ₗ deconcatenation R M

The co-Leibniz identity of a coderivation, as a reusable Iff: this exposes the body of IsCoderivation to consumers in other modules, for which the definition's body is not exposed.

theorem TauCeti.ReducedTensorWords.rTensor_add_lTensor_rTensor_congr {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {b₁ b₂ τ : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (P : Submodule R (ReducedTensorWords R M)) (h : ∀ z ∈ P, b₁ z = b₂ z) (w : TensorProduct R ↥P ↥P) : (LinearMap.rTensor (ReducedTensorWords R M) b₁) ((TensorProduct.mapIncl P P) w) + (LinearMap.lTensor (ReducedTensorWords R M) b₁) ((LinearMap.rTensor (ReducedTensorWords R M) τ) ((TensorProduct.mapIncl P P) w)) = (LinearMap.rTensor (ReducedTensorWords R M) b₂) ((TensorProduct.mapIncl P P) w) + (LinearMap.lTensor (ReducedTensorWords R M) b₂) ((LinearMap.rTensor (ReducedTensorWords R M) τ) ((TensorProduct.mapIncl P P) w))

Two endomorphisms agreeing on a submodule have the same twisted co-Leibniz term on tensors of two elements of that submodule, where an auxiliary twist τ acts on the left half of every cut before b is applied to the right half.

theorem TauCeti.ReducedTensorWords.eq_of_letter_comp_eq_of_twist {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {b₁ b₂ τ : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (h₁ : deconcatenation R M ∘ₗ b₁ = LinearMap.rTensor (ReducedTensorWords R M) b₁ ∘ₗ deconcatenation R M + (LinearMap.lTensor (ReducedTensorWords R M) b₁ ∘ₗ LinearMap.rTensor (ReducedTensorWords R M) τ) ∘ₗ deconcatenation R M) (h₂ : deconcatenation R M ∘ₗ b₂ = LinearMap.rTensor (ReducedTensorWords R M) b₂ ∘ₗ deconcatenation R M + (LinearMap.lTensor (ReducedTensorWords R M) b₂ ∘ₗ LinearMap.rTensor (ReducedTensorWords R M) τ) ∘ₗ deconcatenation R M) (hl : letter R M ∘ₗ b₁ = letter R M ∘ₗ b₂) : b₁ = b₂

Two endomorphisms satisfying the same twisted co-Leibniz identity Δ ∘ b = (b ⊗ 1) ∘ Δ + (1 ⊗ b) ∘ (τ ⊗ 1) ∘ Δ and agreeing after projection onto letters are equal, by induction along the conilpotence filtration. This is the determinedness argument shared by IsCoderivation.eq_of_letter_comp_eq (with τ = LinearMap.id) and IsGradedCoderivation.eq_of_letter_comp_eq.

theorem TauCeti.ReducedTensorWords.IsCoderivation.eq_of_letter_comp_eq {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {b₁ b₂ : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (h₁ : IsCoderivation R b₁) (h₂ : IsCoderivation R b₂) (hl : letter R M ∘ₗ b₁ = letter R M ∘ₗ b₂) : b₁ = b₂

A coderivation of the reduced tensor coalgebra is determined by its Taylor components, that is by its composite with the projection onto single letters. Two coderivations agreeing there agree on every tensor word, by induction along the conilpotence filtration.

theorem TauCeti.ReducedTensorWords.sum_tmul_splice_eq_zero (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {c p : ℕ} (u : ReducedTensorWords R M) (e : ℕ → M) (hp : n ≤ c + p) : ∑ d ∈ Finset.range (n + 1), u ⊗ₜ[R] splice R x c (n - c) p d (e d) = 0

Off the triangle c + p < n, every right-half term of the co-Leibniz rule vanishes: an empty collapse is zero outright, and an overrunning collapse vanishes because the cut half is shorter than the end of the collapsed block.

@[simp]

theorem TauCeti.ReducedTensorWords.isCoderivation_coderiv (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) : IsCoderivation R (coderiv R F)

coderiv F is a coderivation. Both sides of the co-Leibniz rule are the sum, over a cut position and a collapsed block, of the tensor of the two halves with the block collapsed in whichever half contains it; a block is never split by a cut, and a cut never splits the new letter.

theorem TauCeti.ReducedTensorWords.letter_splice_eq_zero (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b p d : ℕ} (e : M) (hdb : d ≠ b) : (letter R M) (splice R x a b p d e) = 0

The letter of a spliced word vanishes unless the whole block was collapsed, since otherwise the word has length at least two.

theorem TauCeti.ReducedTensorWords.letter_splice_eq_zero_of_not_whole (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {p d : ℕ} (e : M) (h : ¬(p = 0 ∧ d = n)) : (letter R M) (splice R x 0 n p d e) = 0

The letter of a spliced word vanishes unless the collapse replaces the entire word.

theorem TauCeti.ReducedTensorWords.letter_splice_self (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b : ℕ} (e : M) (hb : 0 < b) (hab : a + b ≤ n) : (letter R M) (splice R x a b 0 b e) = e

Collapsing a whole block leaves the single new letter.

@[simp]

theorem TauCeti.ReducedTensorWords.letter_comp_coderiv (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) : letter R M ∘ₗ coderiv R F = F

The Taylor components of coderiv F are F: the only summand of the expansion that leaves a single letter is the one collapsing the whole word.

def TauCeti.ReducedTensorWords.coderivations (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule R (ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M)

The submodule of coderivations of the reduced tensor coalgebra. Membership in it is TauCeti.ReducedTensorWords.mem_coderivations.

Equations

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

@[simp]

theorem TauCeti.ReducedTensorWords.mem_coderivations (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} : b ∈ coderivations R M ↔ IsCoderivation R b

noncomputable def TauCeti.ReducedTensorWords.coderivEquivTaylor (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : ↥(coderivations R M) ≃ₗ[R] ReducedTensorWords R M →ₗ[R] M

Coderivations of the reduced tensor coalgebra are exactly their Taylor components: taking the letter of the value is a linear isomorphism onto the maps to single letters, with inverse the Taylor expansion coderiv.

Its body is sealed; reason about it through TauCeti.ReducedTensorWords.coderivEquivTaylor_apply and TauCeti.ReducedTensorWords.coderivEquivTaylor_symm_apply.

Equations

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

@[simp]

theorem TauCeti.ReducedTensorWords.coderivEquivTaylor_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (b : ↥(coderivations R M)) : (coderivEquivTaylor R M) b = letter R M ∘ₗ ↑b

@[simp]

theorem TauCeti.ReducedTensorWords.coderivEquivTaylor_symm_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (F : ReducedTensorWords R M →ₗ[R] M) : (coderivEquivTaylor R M).symm F = ⟨coderiv R F, ⋯⟩

noncomputable def LinearMap.taylorComponent {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : TauCeti.ReducedTensorWords R M →ₗ[R] TauCeti.ReducedTensorWords R M) (n : { n : ℕ // 0 < n }) : TensorPower R (↑n) M →ₗ[R] M

The arity-n piece of the Taylor component letter R M ∘ₗ b: restrict to words of length n, apply the endomorphism, and retain its length-one component.

Equations

• b.taylorComponent n = (TauCeti.ReducedTensorWords.letter R M ∘ₗ b) ∘ₗ TauCeti.ReducedTensorWords.of R M n

@[simp]

theorem LinearMap.taylorComponent_apply {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : TauCeti.ReducedTensorWords R M →ₗ[R] TauCeti.ReducedTensorWords R M) (n : { n : ℕ // 0 < n }) (x : TensorPower R (↑n) M) : (b.taylorComponent n) x = (TauCeti.ReducedTensorWords.letter R M) (b ((TauCeti.ReducedTensorWords.of R M n) x))

Evaluation of a Taylor arity component is restriction to words of the specified length followed by projection to letters.

@[simp]

theorem LinearMap.taylorComponent_zero {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : { n : ℕ // 0 < n }) : taylorComponent 0 n = 0

Every arity component of the zero endomorphism is zero.

@[simp]

theorem LinearMap.taylorComponent_coderiv {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (F : TauCeti.ReducedTensorWords R M →ₗ[R] M) (n : { n : ℕ // 0 < n }) : (TauCeti.ReducedTensorWords.coderiv R F).taylorComponent n = F ∘ₗ TauCeti.ReducedTensorWords.of R M n

The arity components of coderiv F are the restrictions of F to each tensor length.

@[simp]

theorem LinearMap.taylorComponent_add {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (b₁ b₂ : TauCeti.ReducedTensorWords R M →ₗ[R] TauCeti.ReducedTensorWords R M) (n : { n : ℕ // 0 < n }) : (b₁ + b₂).taylorComponent n = b₁.taylorComponent n + b₂.taylorComponent n

Taking an arity component preserves addition of endomorphisms.

@[simp]

theorem LinearMap.taylorComponent_smul {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) (b : TauCeti.ReducedTensorWords R M →ₗ[R] TauCeti.ReducedTensorWords R M) (n : { n : ℕ // 0 < n }) : (r • b).taylorComponent n = r • b.taylorComponent n

Taking an arity component preserves scalar multiplication of endomorphisms.

theorem TauCeti.ReducedTensorWords.IsCoderivation.eq_zero_iff_taylorComponent_eq_zero {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hb : IsCoderivation R b) : b = 0 ↔ ∀ (n : { n : ℕ // 0 < n }), b.taylorComponent n = 0

A coderivation vanishes exactly when each of its aritywise Taylor components vanishes.

theorem TauCeti.ReducedTensorWords.IsCoderivation.eq_zero_iff_taylorComponent_tprod_eq_zero {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {b : ReducedTensorWords R M →ₗ[R] ReducedTensorWords R M} (hb : IsCoderivation R b) : b = 0 ↔ ∀ (n : { n : ℕ // 0 < n }) (x : Fin ↑n → M), (b.taylorComponent n) ((PiTensorProduct.tprod R) x) = 0

A coderivation vanishes exactly when every arity component vanishes on pure tensors.