The coaugmented tensor coalgebra

For an R-module M, the tensor words ⨁_{n ≥ 0} M^{⊗n} carry the deconcatenation coproduct Δ (x₁ ⋯ x_n) = ∑_{c = 0}^{n} (x₁ ⋯ x_c) ⊗ (x_{c+1} ⋯ x_n), whose outer two summands use the empty word. Together with the counit that reads off the length-zero coefficient this makes the tensor words a genuine Coalgebra in Mathlib's sense, coaugmented by r ↦ r · 1, where the empty word 1 is group-like.

This is the counital (coaugmented) extension of the reduced tensor coalgebra TauCeti.ReducedTensorWords, which only admits the nontrivial cuts and is therefore not counital. The comparison is TauCeti.TensorWords.deconcatenation_comp_reducedInclusion: the coproduct of a word x of positive length is 1 ⊗ x + x ⊗ 1 together with the reduced coproduct of x, and the reduced words map onto exactly the kernel ker ε of the counit. Both facts are what makes the two presentations interchangeable downstream: an A∞ structure is a square-zero coderivation of the reduced coalgebra, while an A∞ morphism is a morphism of the coaugmented ones.

The combinatorics is the same as in the reduced case and is again organised through blocks of consecutive letters, TauCeti.TensorWords.subword. In both cases the two iterated coproducts are indexed by the triangle 0 ≤ d ≤ c ≤ n of nested cuts and are compared after extending them to the full square. The one difference is that an empty block is now the empty word rather than zero, so the degenerate summands outside the triangle no longer vanish: the extension is not free as it is in the reduced case, and it is carried out by Finset.sum_filter, which keeps the constraint d ≤ c as an explicit if. Coassociativity is then Finset.sum_comm all the same.

Main definitions

• TauCeti.TensorWords: the direct sum of all tensor powers, the empty one included.
• TauCeti.TensorWords.deconcatenation: the sum over every cut of a tensor word.
• TauCeti.TensorWords.counit: the length-zero coefficient.
• TauCeti.TensorWords.coaugmentation: the algebra map, bundled as a coalgebra morphism.
• TauCeti.TensorWords.reducedInclusion and TauCeti.TensorWords.reducedProjection: the positive-length words as a direct summand.
• TauCeti.TensorWords.map: apply a linear map to every letter of a tensor word.

Main results

• TauCeti.TensorWords.instCoalgebra: tensor words are a coalgebra.
• TauCeti.TensorWords.isGroupLikeElem_one: the empty word is group-like.
• TauCeti.TensorWords.deconcatenation_comp_reducedInclusion: on a word of positive length the coproduct is the reduced coproduct together with its two degenerate cuts.
• TauCeti.TensorWords.ker_counit: the kernel of the counit is the image of the positive-length words under TauCeti.TensorWords.reducedInclusion.
• TauCeti.TensorWords.map_id, TauCeti.TensorWords.map_comp, TauCeti.TensorWords.deconcatenation_natural and TauCeti.TensorWords.counit_comp_map: the letterwise maps are homomorphisms, and deconcatenation and the counit are natural with respect to them.
• TauCeti.TensorWords.map_comp_reducedInclusion: on the words of positive length a letterwise map is the inclusion of the corresponding reduced 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.

@[reducible, inline]

abbrev TauCeti.TensorWords (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max uM uR)

The module of tensor words, the empty word included.

Equations

• TauCeti.TensorWords R M = DirectSum ℕ fun (n : ℕ) => TensorPower R n M

noncomputable def TauCeti.TensorWords.of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : TensorPower R n M →ₗ[R] TensorWords R M

Include a tensor power into tensor words.

Equations

• TauCeti.TensorWords.of R M n = DirectSum.lof R ℕ (fun (n : ℕ) => TensorPower R n M) n

theorem TauCeti.TensorWords.of_def (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : of R M n = DirectSum.lof R ℕ (fun (n : ℕ) => TensorPower R n M) n

Inclusion into tensor words is the direct-sum inclusion.

theorem TauCeti.TensorWords.of_tprod_congr (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {x y : Fin n → M} (h : ∀ (i : Fin n), x i = y i) : (of R M n) ((PiTensorProduct.tprod R) x) = (of R M n) ((PiTensorProduct.tprod R) y)

Pure tensor words with pointwise equal letters are equal.

theorem TauCeti.TensorWords.iSup_range_of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : ⨆ (n : ℕ), (of R M n).range = ⊤

The words of a fixed length generate all tensor words.

theorem TauCeti.TensorWords.linearMap_ext (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] {f g : TensorWords R M →ₗ[R] N} (h : ∀ (n : ℕ) (x : Fin n → M), f ((of R M n) ((PiTensorProduct.tprod R) x)) = g ((of R M n) ((PiTensorProduct.tprod R) x))) : f = g

Two linear maps out of tensor words agree if they agree on pure tensor words.

noncomputable def TauCeti.TensorWords.component (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : TensorWords R M →ₗ[R] TensorPower R n M

Project tensor words to a fixed tensor length.

Equations

• TauCeti.TensorWords.component R M n = DirectSum.component R ℕ (fun (n : ℕ) => TensorPower R n M) n

@[simp]

theorem TauCeti.TensorWords.component_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : TensorWords R M) : (component R M n) x = x n

Applying the length projection reads the corresponding coordinate.

The specialized projection rules for included words take precedence.

@[simp]

theorem TauCeti.TensorWords.component_of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : TensorPower R n M) : (component R M n) ((of R M n) x) = x

The component of an included tensor power at its own length is that tensor power.

@[simp]

theorem TauCeti.TensorWords.component_of_of_ne (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {m n : ℕ} (h : m ≠ n) (x : TensorPower R m M) : (component R M n) ((of R M m) x) = 0

Projecting an included tensor power vanishes when the two lengths differ.

@[simp]

theorem TauCeti.TensorWords.toModule_of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] (φ : (n : ℕ) → TensorPower R n M →ₗ[R] N) (n : ℕ) (z : TensorPower R n M) : (DirectSum.toModule R ℕ N φ) ((of R M n) z) = (φ n) z

A linear map assembled from its length components is that component on a tensor word of that length.

The counit

noncomputable def TauCeti.TensorWords.counit (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorWords R M →ₗ[R] R

The counit of the tensor coalgebra reads off the coefficient of the empty word.

Equations

• TauCeti.TensorWords.counit R M = ↑TensorPower.algebraMap₀.symm ∘ₗ TauCeti.TensorWords.component R M 0

theorem TauCeti.TensorWords.counit_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TensorWords R M) : (counit R M) x = TensorPower.algebraMap₀.symm ((component R M 0) x)

The counit evaluates the length-zero component using the scalar identification.

@[simp]

theorem TauCeti.TensorWords.counit_of_zero (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (z : TensorPower R 0 M) : (counit R M) ((of R M 0) z) = TensorPower.algebraMap₀.symm z

On the empty length the counit is the canonical identification with the ground ring.

@[simp]

theorem TauCeti.TensorWords.counit_of_of_ne_zero (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (hn : n ≠ 0) (z : TensorPower R n M) : (counit R M) ((of R M n) z) = 0

The counit annihilates every word of positive length.

theorem TauCeti.TensorWords.algebraMap_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) : (algebraMap R (TensorWords R M)) r = (of R M 0) (TensorPower.algebraMap₀ r)

The algebra map is inclusion into tensor length zero.

theorem TauCeti.TensorWords.one_eq_of_zero (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : 1 = (of R M 0) ((PiTensorProduct.tprod R) fun (i : Fin 0) => i.elim0)

The algebra unit is the empty pure tensor in tensor length zero.

@[simp]

theorem TauCeti.TensorWords.counit_comp_algebraMap (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : counit R M ∘ₗ Algebra.linearMap R (TensorWords R M) = LinearMap.id

The counit is a retraction of the coaugmentation given by the algebra map.

@[simp]

theorem TauCeti.TensorWords.counit_algebraMap (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) : (counit R M) ((algebraMap R (TensorWords R M)) r) = r

The counit retracts the coaugmentation on every scalar.

@[simp]

theorem TauCeti.TensorWords.counit_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : (counit R M) 1 = 1

The empty word has counit one.

Deconcatenation

noncomputable def TauCeti.TensorWords.deconcatenationComponent (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : TensorPower R n M →ₗ[R] TensorProduct R (TensorWords R M) (TensorWords R M)

Deconcatenation on words of one fixed length, summed over all cuts, the two outer ones included.

Equations

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

@[simp]

theorem TauCeti.TensorWords.deconcatenationComponent_tprod (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : Fin n → M) : (deconcatenationComponent R M n) ((PiTensorProduct.tprod R) x) = ∑ i : Fin (n + 1), (of R M ↑i) ((PiTensorProduct.tprod R) fun (j : Fin ↑i) => x (Fin.castLE ⋯ j)) ⊗ₜ[R] (of R M (n - ↑i)) ((PiTensorProduct.tprod R) fun (j : Fin (n - ↑i)) => x ⟨↑i + ↑j, ⋯⟩)

On a pure tensor, deconcatenation is the sum of its prefix--suffix cuts.

noncomputable def TauCeti.TensorWords.deconcatenation (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorWords R M →ₗ[R] TensorProduct R (TensorWords R M) (TensorWords R M)

Deconcatenation cuts a tensor word at every position, the two outer positions included.

Equations

• TauCeti.TensorWords.deconcatenation R M = DirectSum.toModule R ℕ (TensorProduct R (TauCeti.TensorWords R M) (TauCeti.TensorWords R M)) (TauCeti.TensorWords.deconcatenationComponent R M)

@[simp]

theorem TauCeti.TensorWords.deconcatenation_of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : TensorPower R n M) : (deconcatenation R M) ((of R M n) x) = (deconcatenationComponent R M n) x

Deconcatenation is computed length by length.

theorem TauCeti.TensorWords.map_component_comp_deconcatenation (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (p q : ℕ) : TensorProduct.map (component R M p) (component R M q) ∘ₗ deconcatenation R M = ↑TensorPower.mulEquiv.symm ∘ₗ component R M (p + q)

Each bidegree of deconcatenation splits the component of the total length.

noncomputable def TauCeti.TensorWords.subword (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) (a b : ℕ) : TensorWords R M

The tensor word x a ⊗ ⋯ ⊗ x (a + b - 1), of length b and starting at position a.

It is zero when the requested block runs past the end of x, and is 1 when the block is empty and starts inside the tuple (a ≤ n); the intended range of the definition is a + b ≤ n.

Equations

• TauCeti.TensorWords.subword R x a b = if h : a + b ≤ n then (TauCeti.TensorWords.of R M b) ((PiTensorProduct.tprod R) fun (j : Fin b) => x ⟨a + ↑j, ⋯⟩) else 0

theorem TauCeti.TensorWords.subword_eq_of_tprod (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b : ℕ} (hab : a + b ≤ n) : subword R x a b = (of R M b) ((PiTensorProduct.tprod R) fun (j : Fin b) => x ⟨a + ↑j, ⋯⟩)

On its intended range, a subword is the pure tensor of the selected block of letters.

@[simp]

theorem TauCeti.TensorWords.subword_eq_zero_of_lt_add (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b : ℕ} (hab : n < a + b) : subword R x a b = 0

A block running past the end of the tuple is zero.

@[simp]

theorem TauCeti.TensorWords.subword_length_zero (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a : ℕ} (ha : a ≤ n) : subword R x a 0 = 1

An empty block inside a tuple is the empty word.

theorem TauCeti.TensorWords.of_tprod_eq_subword (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) : (of R M n) ((PiTensorProduct.tprod R) x) = subword R x 0 n

A whole tuple is the subword of full length starting at its beginning.

@[simp]

theorem TauCeti.TensorWords.counit_subword_of_pos (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b : ℕ} (hb : 0 < b) : (counit R M) (subword R x a b) = 0

A nonempty block is annihilated by the counit.

theorem TauCeti.TensorWords.deconcatenation_subword (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b : ℕ} : (deconcatenation R M) (subword R x a b) = ∑ c ∈ Finset.range (b + 1), subword R x a c ⊗ₜ[R] subword R x (a + c) (b - c)

Deconcatenating a block cuts it at each of its positions, the two outer ones included.

Coassociativity and counitality

theorem TauCeti.TensorWords.deconcatenation_coassoc (R : Type uR) [CommSemiring R] (M : Type uM) [AddCommMonoid M] [Module R M] : ↑(TensorProduct.assoc R (TensorWords R M) (TensorWords R M) (TensorWords R M)) ∘ₗ LinearMap.rTensor (TensorWords R M) (deconcatenation R M) ∘ₗ deconcatenation R M = LinearMap.lTensor (TensorWords R M) (deconcatenation R M) ∘ₗ deconcatenation R M

Deconcatenation is coassociative: cutting a tensor word twice gives the same sum of triples of blocks whether the second cut is taken in the left or in the right factor of the first.

theorem TauCeti.TensorWords.rTensor_counit_comp_deconcatenation (R : Type uR) [CommSemiring R] (M : Type uM) [AddCommMonoid M] [Module R M] : LinearMap.rTensor (TensorWords R M) (counit R M) ∘ₗ deconcatenation R M = (TensorProduct.mk R R (TensorWords R M)) 1

counit is a left counit for deconcatenation; only the cut with an empty left block survives.

theorem TauCeti.TensorWords.lTensor_counit_comp_deconcatenation (R : Type uR) [CommSemiring R] (M : Type uM) [AddCommMonoid M] [Module R M] : LinearMap.lTensor (TensorWords R M) (counit R M) ∘ₗ deconcatenation R M = (TensorProduct.mk R (TensorWords R M) R).flip 1

counit is a right counit for deconcatenation; only the cut with an empty right block survives.

@[instance_reducible]

noncomputable instance TauCeti.TensorWords.instCoalgebraStruct (R : Type uR) [CommSemiring R] (M : Type uM) [AddCommMonoid M] [Module R M] : CoalgebraStruct R (TensorWords R M)

Deconcatenation and the length-zero coefficient are the coalgebra data of tensor words.

Equations

• TauCeti.TensorWords.instCoalgebraStruct R M = { comul := TauCeti.TensorWords.deconcatenation R M, counit := TauCeti.TensorWords.counit R M }

@[simp]

theorem TauCeti.TensorWords.comul_eq_deconcatenation (R : Type uR) [CommSemiring R] (M : Type uM) [AddCommMonoid M] [Module R M] : CoalgebraStruct.comul = deconcatenation R M

The comultiplication of the coalgebra structure is deconcatenation.

@[simp]

theorem TauCeti.TensorWords.counit_eq_counit (R : Type uR) [CommSemiring R] (M : Type uM) [AddCommMonoid M] [Module R M] : CoalgebraStruct.counit = counit R M

The counit of the coalgebra structure is the length-zero coefficient.

@[instance_reducible]

noncomputable instance TauCeti.TensorWords.instCoalgebra (R : Type uR) [CommSemiring R] (M : Type uM) [AddCommMonoid M] [Module R M] : Coalgebra R (TensorWords R M)

Tensor words form a coalgebra over the ground ring.

Equations

• TauCeti.TensorWords.instCoalgebra R M = { toCoalgebraStruct := TauCeti.TensorWords.instCoalgebraStruct R M, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

The empty word is group-like

@[simp]

theorem TauCeti.TensorWords.deconcatenation_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : (deconcatenation R M) 1 = 1 ⊗ₜ[R] 1

Deconcatenating the empty word cuts it in the only way available.

theorem TauCeti.TensorWords.isGroupLikeElem_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : IsGroupLikeElem R 1

The empty word is a group-like element of the tensor coalgebra.

noncomputable def TauCeti.TensorWords.coaugmentation (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : R →ₗc[R] TensorWords R M

The canonical coaugmentation, bundling the algebra map as a coalgebra morphism.

Equations

• TauCeti.TensorWords.coaugmentation R M = { toLinearMap := Algebra.linearMap R (TauCeti.TensorWords R M), counit_comp := ⋯, map_comp_comul := ⋯ }

@[simp]

theorem TauCeti.TensorWords.coaugmentation_toLinearMap (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : ↑(coaugmentation R M) = Algebra.linearMap R (TensorWords R M)

The linear map underlying the canonical coaugmentation is the algebra map.

@[simp]

theorem TauCeti.TensorWords.coaugmentation_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) : (coaugmentation R M) r = (algebraMap R (TensorWords R M)) r

The canonical coaugmentation sends a scalar through the algebra map.

Comparison with the reduced tensor coalgebra

noncomputable def TauCeti.TensorWords.reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : ReducedTensorWords R M →ₗ[R] TensorWords R M

The words of positive length inside all tensor words.

Equations

• TauCeti.TensorWords.reducedInclusion R M = DirectSum.toModule R { n : ℕ // 0 < n } (TauCeti.TensorWords R M) fun (n : { n : ℕ // 0 < n }) => TauCeti.TensorWords.of R M ↑n

@[simp]

theorem TauCeti.TensorWords.reducedInclusion_of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : { n : ℕ // 0 < n }) (z : TensorPower R (↑n) M) : (reducedInclusion R M) ((ReducedTensorWords.of R M n) z) = (of R M ↑n) z

The inclusion of the reduced tensor words keeps each length component.

@[simp]

theorem TauCeti.TensorWords.component_reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (k : ℕ) (w : ReducedTensorWords R M) : (component R M k) ((reducedInclusion R M) w) = if hk : 0 < k then (ReducedTensorWords.component R M ⟨k, hk⟩) w else 0

The included reduced word has precisely its positive-length components.

noncomputable def TauCeti.TensorWords.reducedProjection (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorWords R M →ₗ[R] ReducedTensorWords R M

The retraction of TauCeti.TensorWords.reducedInclusion that deletes the empty word.

Equations

• TauCeti.TensorWords.reducedProjection R M = DirectSum.toModule R ℕ (TauCeti.ReducedTensorWords R M) fun (n : ℕ) => if h : 0 < n then TauCeti.ReducedTensorWords.of R M ⟨n, h⟩ else 0

@[simp]

theorem TauCeti.TensorWords.reducedProjection_of_of_pos (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (hn : 0 < n) (z : TensorPower R n M) : (reducedProjection R M) ((of R M n) z) = (ReducedTensorWords.of R M ⟨n, hn⟩) z

The projection keeps every component of positive length.

@[simp]

theorem TauCeti.TensorWords.reducedProjection_of_zero (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (z : TensorPower R 0 M) : (reducedProjection R M) ((of R M 0) z) = 0

The projection deletes the length-zero component.

@[simp]

theorem TauCeti.TensorWords.reducedProjection_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : (reducedProjection R M) 1 = 0

The projection deletes the empty word.

@[simp]

theorem TauCeti.TensorWords.component_reducedProjection (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (p : { n : ℕ // 0 < n }) (w : TensorWords R M) : (ReducedTensorWords.component R M p) ((reducedProjection R M) w) = (component R M ↑p) w

Deleting the empty word preserves each positive-length component.

@[simp]

theorem TauCeti.TensorWords.reducedProjection_comp_reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : reducedProjection R M ∘ₗ reducedInclusion R M = LinearMap.id

The projection is a retraction of the inclusion.

@[simp]

theorem TauCeti.TensorWords.reducedProjection_reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (w : ReducedTensorWords R M) : (reducedProjection R M) ((reducedInclusion R M) w) = w

Projecting an included positive-length word returns that word.

theorem TauCeti.TensorWords.reducedInclusion_injective (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : Function.Injective ⇑(reducedInclusion R M)

The reduced tensor words inject into all tensor words.

@[simp]

theorem TauCeti.TensorWords.counit_comp_reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : counit R M ∘ₗ reducedInclusion R M = 0

Every word of positive length lies in the augmentation coideal.

@[simp]

theorem TauCeti.TensorWords.counit_reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (w : ReducedTensorWords R M) : (counit R M) ((reducedInclusion R M) w) = 0

The counit vanishes on every positive-length word.

theorem TauCeti.TensorWords.reducedInclusion_comp_reducedProjection_add_algebraMap_comp_counit (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : reducedInclusion R M ∘ₗ reducedProjection R M + Algebra.linearMap R (TensorWords R M) ∘ₗ counit R M = LinearMap.id

Tensor words are the empty word together with the words of positive length.

@[simp]

theorem TauCeti.TensorWords.reducedInclusion_reducedProjection_add_algebraMap_counit (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (w : TensorWords R M) : (reducedInclusion R M) ((reducedProjection R M) w) + (algebraMap R (TensorWords R M)) ((counit R M) w) = w

Every tensor word is the sum of its positive-length part and its length-zero part.

theorem TauCeti.TensorWords.ker_counit (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : (counit R M).ker = (reducedInclusion R M).range

The kernel of the counit is exactly the image of the positive-length words under TauCeti.TensorWords.reducedInclusion.

@[simp]

theorem TauCeti.TensorWords.reducedInclusion_subword (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b : ℕ} (hb : 0 < b) : (reducedInclusion R M) (ReducedTensorWords.subword R x a b) = subword R x a b

A nonempty block is the same word read in either presentation.

theorem TauCeti.TensorWords.deconcatenation_comp_reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : deconcatenation R M ∘ₗ reducedInclusion R M = (TensorProduct.mk R (TensorWords R M) (TensorWords R M)) 1 ∘ₗ reducedInclusion R M + (TensorProduct.mk R (TensorWords R M) (TensorWords R M)).flip 1 ∘ₗ reducedInclusion R M + TensorProduct.map (reducedInclusion R M) (reducedInclusion R M) ∘ₗ ReducedTensorWords.deconcatenation R M

On a word of positive length the coproduct is the reduced coproduct together with the two degenerate cuts.

theorem TauCeti.TensorWords.deconcatenation_comp_reducedInclusion_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (w : ReducedTensorWords R M) : (deconcatenation R M) ((reducedInclusion R M) w) = 1 ⊗ₜ[R] (reducedInclusion R M) w + (reducedInclusion R M) w ⊗ₜ[R] 1 + (TensorProduct.map (reducedInclusion R M) (reducedInclusion R M)) ((ReducedTensorWords.deconcatenation R M) w)

The coproduct of an included positive-length word is its two degenerate cuts together with the included reduced coproduct.

@[simp]

theorem TauCeti.TensorWords.map_reducedProjection_deconcatenation_reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (w : ReducedTensorWords R M) : (TensorProduct.map (reducedProjection R M) (reducedProjection R M)) ((deconcatenation R M) ((reducedInclusion R M) w)) = (ReducedTensorWords.deconcatenation R M) w

Projecting both factors of the coproduct of a positive-length word recovers reduced deconcatenation.

@[simp]

theorem TauCeti.TensorWords.map_reducedProjection_comp_deconcatenation_comp_reducedInclusion (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorProduct.map (reducedProjection R M) (reducedProjection R M) ∘ₗ deconcatenation R M ∘ₗ reducedInclusion R M = ReducedTensorWords.deconcatenation R M

Projecting both factors after deconcatenating an included positive-length word is reduced deconcatenation.

@[simp]

theorem TauCeti.TensorWords.deconcatenation_of_length_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (z : TensorPower R 1 M) : (deconcatenation R M) ((of R M 1) z) = 1 ⊗ₜ[R] (of R M 1) z + (of R M 1) z ⊗ₜ[R] 1

The letters of a tensor word are primitive.

This fires ahead of TauCeti.TensorWords.deconcatenation_of, whose right-hand side deconcatenationComponent has no computation rule for an abstract tensor power.

Letterwise maps

noncomputable def TauCeti.TensorWords.map {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : TensorWords R M →ₗ[R] TensorWords R N

Apply a linear map to every letter of a tensor word, the empty word included.

Equations

• TauCeti.TensorWords.map f = DirectSum.lmap fun (x : ℕ) => PiTensorProduct.map fun (x : Fin x) => f

@[simp]

theorem TauCeti.TensorWords.map_of {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (n : ℕ) (x : TensorPower R n M) : (map f) ((of R M n) x) = (of R N n) ((PiTensorProduct.map fun (x : Fin n) => f) x)

Mapping a word of a fixed length applies the tensor power of the map in that length.

theorem TauCeti.TensorWords.map_of_tprod {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (n : ℕ) (x : Fin n → M) : (map f) ((of R M n) ((PiTensorProduct.tprod R) x)) = (of R N n) ((PiTensorProduct.tprod R) fun (i : Fin n) => f (x i))

Mapping a pure tensor applies the map to each of its letters.

@[simp]

theorem TauCeti.TensorWords.map_one {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : (map f) 1 = 1

Mapping the empty word leaves the empty word unchanged.

@[simp]

theorem TauCeti.TensorWords.map_id {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] : map LinearMap.id = LinearMap.id

Mapping the identity map over the letters is the identity.

@[simp]

theorem TauCeti.TensorWords.map_comp {R : Type uR} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] (g : N →ₗ[R] P) (f : M →ₗ[R] N) : map (g ∘ₗ f) = map g ∘ₗ map f

Mapping a composite over the letters composes the two letterwise maps.

theorem TauCeti.TensorWords.deconcatenation_natural {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : deconcatenation R N ∘ₗ map f = TensorProduct.map (map f) (map f) ∘ₗ deconcatenation R M

Deconcatenation is natural with respect to linear maps of the letters.

@[simp]

theorem TauCeti.TensorWords.counit_comp_map {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : counit R N ∘ₗ map f = counit R M

The counit is natural with respect to the letterwise maps.

theorem TauCeti.TensorWords.map_comp_reducedInclusion {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : map f ∘ₗ reducedInclusion R M = reducedInclusion R N ∘ₗ ReducedTensorWords.map R f

On the words of positive length the letterwise map of the coaugmented coalgebra is the inclusion of the letterwise map of the reduced one, because the two apply the same map to the same letters.