Primitive elements 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. This file computes its primitive elements: a tensor word killed by deconcatenation is a single letter.

Indeed the (1, n - 1) bidegree part of Δ on a word of length n is the cut after its first letter, and cutting is injective, so no component of length at least two can survive.

Main definitions

• TauCeti.ReducedTensorWords.letter, TauCeti.ReducedTensorWords.ofLetter: the length-one component of a tensor word, and a single letter viewed as a tensor word.

Main results

• TauCeti.ReducedTensorWords.subword_one: a block of length one is a single letter.
• TauCeti.ReducedTensorWords.deconcatenation_prepend: the cuts of a prepended word.
• TauCeti.ReducedTensorWords.prepend_ofLetter and TauCeti.ReducedTensorWords.deconcatenation_of_two: the two-letter word and its only cut.
• TauCeti.ReducedTensorWords.letter_comp_map: the letter of a letterwise-mapped word is the image of its letter.
• TauCeti.ReducedTensorWords.deconcatenation_eq_zero_iff: the primitives of the reduced tensor coalgebra are exactly the single 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.letter (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : ReducedTensorWords R M →ₗ[R] M

The letter of a reduced tensor word: its length-one component, read as an element of M.

Equations

• TauCeti.ReducedTensorWords.letter R M = ↑(TauCeti.TensorPower.oneEquiv R M) ∘ₗ TauCeti.ReducedTensorWords.component R M 1

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

A single letter, viewed as a reduced tensor word of length one.

Equations

• TauCeti.ReducedTensorWords.ofLetter R M = TauCeti.ReducedTensorWords.of R M 1 ∘ₗ ↑(TauCeti.TensorPower.oneEquiv R M).symm

theorem TauCeti.ReducedTensorWords.ofLetter_eq_of_tprod (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) : (ofLetter R M) a = (of R M 1) ((PiTensorProduct.tprod R) fun (x : Fin ↑1) => a)

A single letter is the pure tensor word of length one on that letter.

theorem TauCeti.ReducedTensorWords.component_ofLetter (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) : (component R M 1) ((ofLetter R M) a) = (TensorPower.oneEquiv R M).symm a

The length-one component of a single letter is that letter under the tensor-power identification.

@[simp]

theorem TauCeti.ReducedTensorWords.component_ofLetter_of_ne (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {n : { n : ℕ // 0 < n }} (hn : n ≠ 1) (a : M) : (component R M n) ((ofLetter R M) a) = 0

Every component of a single letter away from length one vanishes.

theorem TauCeti.ReducedTensorWords.letter_apply (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : ReducedTensorWords R M) : (letter R M) x = (TensorPower.oneEquiv R M) ((component R M 1) x)

The letter of a tensor word is its length-one component, read through the length-one identification.

@[simp]

theorem TauCeti.ReducedTensorWords.letter_ofLetter (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) : (letter R M) ((ofLetter R M) a) = a

Reading off the letter of a single letter returns it.

@[simp]

theorem TauCeti.ReducedTensorWords.deconcatenation_ofLetter (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) : (deconcatenation R M) ((ofLetter R M) a) = 0

A single letter has no nontrivial cut.

theorem TauCeti.ReducedTensorWords.map_component_deconcatenation (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : { n : ℕ // 0 < n }) (hn : 2 ≤ ↑n) : TensorProduct.map (component R M 1) (component R M ⟨↑n - 1, ⋯⟩) ∘ₗ deconcatenation R M = TensorPower.splitAt R M (↑n) 1 ⋯ ∘ₗ component R M n

Reading off the (1, n - 1) bidegree part of reduced deconcatenation recovers the cut of a word of length n after its first letter.

theorem TauCeti.ReducedTensorWords.eq_of_deconcatenation_eq_of_letter_eq (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {x y : ReducedTensorWords R M} (hd : (deconcatenation R M) x = (deconcatenation R M) y) (hl : (letter R M) x = (letter R M) y) : x = y

A reduced tensor word is determined by its deconcatenation together with its letter: the components of length at least two are read off from the cut after the first letter, and the length-one component is the letter.

theorem TauCeti.ReducedTensorWords.subword_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (z : Fin n → M) {a : ℕ} (ha : a < n) : subword R z a 1 = (ofLetter R M) (z ⟨a, ha⟩)

A block of length one is the corresponding single letter.

theorem TauCeti.ReducedTensorWords.letter_subword_of_ne_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (z : Fin n → M) (a : ℕ) {b : ℕ} (hb : b ≠ 1) : (letter R M) (subword R z a b) = 0

A block whose length is not one has no letter component.

@[simp]

theorem TauCeti.ReducedTensorWords.letter_prepend {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) (w : ReducedTensorWords R M) : (letter R M) (((prepend R M) a) w) = 0

A prepended word has length at least two, so it has no letter component.

theorem TauCeti.ReducedTensorWords.deconcatenation_prepend {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) (w : ReducedTensorWords R M) : (deconcatenation R M) (((prepend R M) a) w) = (ofLetter R M) a ⊗ₜ[R] w + (LinearMap.rTensor (ReducedTensorWords R M) ((prepend R M) a)) ((deconcatenation R M) w)

Cutting a prepended word a · w either separates the new letter from w, or cuts w and prepends a to the left half.

theorem TauCeti.ReducedTensorWords.prepend_ofLetter {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (a b : M) : ((prepend R M) a) ((ofLetter R M) b) = (of R M 2) ((PiTensorProduct.tprod R) ![a, b])

Prepending a letter to a single letter is the two-letter word.

theorem TauCeti.ReducedTensorWords.deconcatenation_of_two {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (a b : M) : (deconcatenation R M) ((of R M 2) ((PiTensorProduct.tprod R) ![a, b])) = (ofLetter R M) a ⊗ₜ[R] (ofLetter R M) b

The only cut of a two-letter word separates its two letters.

@[simp]

theorem TauCeti.ReducedTensorWords.letter_of_two {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (a b : M) : (letter R M) ((of R M 2) ((PiTensorProduct.tprod R) ![a, b])) = 0

A two-letter word has no letter component.

theorem TauCeti.ReducedTensorWords.letter_of_of_ne_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {n : { n : ℕ // 0 < n }} (hn : n ≠ 1) (z : TensorPower R (↑n) M) : (letter R M) ((of R M n) z) = 0

A word whose length is not one has no letter component.

theorem TauCeti.ReducedTensorWords.deconcatenation_eq_zero_iff (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {x : ReducedTensorWords R M} : (deconcatenation R M) x = 0 ↔ x ∈ (ofLetter R M).range

The primitive elements of the reduced tensor coalgebra are exactly the single letters.

@[simp]

theorem TauCeti.ReducedTensorWords.map_ofLetter {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (g : M →ₗ[R] N) (a : M) : (map R g) ((ofLetter R M) a) = (ofLetter R N) (g a)

Mapping a single letter applies the map to that letter.

@[simp]

theorem TauCeti.ReducedTensorWords.letter_comp_map {R : Type uR} {M : Type uM} {N : Type uN} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (g : M →ₗ[R] N) : letter R N ∘ₗ map R g = g ∘ₗ letter R M

The letter of a letterwise-mapped word is the image of its letter.