Reduced tensor words and deconcatenation

For an R-module M, reduced tensor words are the direct sum of its positive tensor powers. This file constructs that module, TauCeti.ReducedTensorWords, and its reduced deconcatenation map, which cuts a positive word at every nontrivial position. It also defines blocks of consecutive letters in a tensor word, used to express iterated cuts. The tensor words that also carry the empty word are the separate type TauCeti.TensorWords, built in TauCeti.LinearAlgebra.TensorCoalgebra.Coaugmented.Basic.

The construction uses Mathlib's TensorPower and direct-sum/tensor-product equivalences, together with TensorPower.splitAt. It is the coalgebra-side input for the suspended bar construction in the DGAInfinity roadmap.

Main definitions

• TauCeti.ReducedTensorWords: the direct sum of positive tensor powers.
• TauCeti.ReducedTensorWords.deconcatenation: sum over every nontrivial cut of a tensor word.
• TauCeti.ReducedTensorWords.subword: a block of consecutive letters in a tensor word.
• TauCeti.ReducedTensorWords.prepend: prepend a letter to a reduced tensor word.

Main results

• TauCeti.ReducedTensorWords.of_tprod_congr: a pure tensor word depends only on its letters, even when the two sides present its length by different arithmetic expressions.
• TauCeti.ReducedTensorWords.subword_congr: equal-length blocks in different ambient tuples or at different offsets agree when their letters agree.
• TauCeti.ReducedTensorWords.subword_tail: blocks of the tail of a tuple.
• TauCeti.ReducedTensorWords.prepend_subword: prepending the preceding letter extends a block.
• TauCeti.ReducedTensorWords.map_subword: mapping a block applies the map to each of its letters.
• TauCeti.ReducedTensorWords.deconcatenation_subword: deconcatenation of a block.

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.ReducedTensorWords (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max uM uR)

The module of nonempty tensor words.

Equations

• TauCeti.ReducedTensorWords R M = DirectSum { n : ℕ // 0 < n } fun (n : { n : ℕ // 0 < n }) => TensorPower R (↑n) M

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

Include a positive tensor power into reduced tensor words.

Equations

• TauCeti.ReducedTensorWords.of R M n = DirectSum.lof R { n : ℕ // 0 < n } (fun (n : { n : ℕ // 0 < n }) => TensorPower R (↑n) M) n

theorem TauCeti.ReducedTensorWords.iSup_range_of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : ⨆ (n : { n : ℕ // 0 < n }), (of R M n).range = ⊤

The positive tensor-power inclusions generate all reduced tensor words.

theorem TauCeti.ReducedTensorWords.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 : ReducedTensorWords R M →ₗ[R] N} (h : ∀ (n : { n : ℕ // 0 < 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 reduced tensor words agree if they agree on pure tensor words.

theorem TauCeti.ReducedTensorWords.of_tprod_congr (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {k l : ℕ} (hk : 0 < k) (hkl : k = l) {u : Fin k → M} {v : Fin l → M} (h : ∀ (i : Fin k), u i = v (Fin.cast hkl i)) : (of R M ⟨k, hk⟩) ((PiTensorProduct.tprod R) u) = (of R M ⟨l, ⋯⟩) ((PiTensorProduct.tprod R) v)

Two pure tensor words of the same length with the same letters are equal. The two lengths are separate arguments, so that this closes goals whose two sides were assembled from different arithmetic expressions for one length.

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

Project reduced tensor words to a fixed positive tensor length.

Equations

• TauCeti.ReducedTensorWords.component R M n = DirectSum.component R { n : ℕ // 0 < n } (fun (n : { n : ℕ // 0 < n }) => TensorPower R (↑n) M) n

@[simp]

theorem TauCeti.ReducedTensorWords.apply_eq_component (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : ReducedTensorWords R M) (n : { n : ℕ // 0 < n }) : x n = (component R M n) x

Evaluating a reduced tensor word at a length agrees with its named component projection.

@[simp]

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

theorem TauCeti.ReducedTensorWords.component_of_eq (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {m n : { k : ℕ // 0 < k }} (h : m = n) (z : TensorPower R (↑m) M) : (component R M n) ((of R M m) z) = (TensorPower.cast R M ⋯) z

Reading off the component of a tensor word at its own length, presented by a second arithmetic expression for that length.

@[simp]

theorem TauCeti.ReducedTensorWords.component_of_of_ne (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {m n : { n : ℕ // 0 < 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.ReducedTensorWords.toModule_of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type uN} [AddCommMonoid N] [Module R N] (φ : (n : { n : ℕ // 0 < n }) → TensorPower R (↑n) M →ₗ[R] N) (n : { n : ℕ // 0 < n }) (z : TensorPower R (↑n) M) : (DirectSum.toModule R { n : ℕ // 0 < n } 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.

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

Deconcatenation on words of one fixed length, summed over all nontrivial cuts.

Equations

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

@[simp]

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

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

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

Reduced deconcatenation cuts a nonempty tensor word at every nontrivial position.

Words of lengths zero and one have no nontrivial cuts; only positive lengths occur in the source, so length one is sent to zero.

Equations

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

@[simp]

theorem TauCeti.ReducedTensorWords.deconcatenation_of (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : { n : ℕ // 0 < n }) (x : TensorPower R (↑n) M) : (deconcatenation R M) ((of R M n) x) = (deconcatenationComponent R M n) x

theorem TauCeti.ReducedTensorWords.deconcatenation_of_length_one (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TensorPower R 1 M) : (deconcatenation R M) ((of R M ⟨1, deconcatenation_of_length_one._proof_2⟩) x) = 0

On tensor words of length one, reduced deconcatenation is zero.

noncomputable def TauCeti.ReducedTensorWords.subword (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) (a b : ℕ) : ReducedTensorWords 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 is empty or runs past the end of x; the intended range of the definition is 0 < b and a + b ≤ n.

Equations

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

theorem TauCeti.ReducedTensorWords.subword_eq_of_tprod (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b : ℕ} (hb : 0 < b) (hab : a + b ≤ n) : subword R x a b = (of R M ⟨b, hb⟩) ((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.ReducedTensorWords.subword_length_zero (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) (a : ℕ) : subword R x a 0 = 0

@[simp]

theorem TauCeti.ReducedTensorWords.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.

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

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

theorem TauCeti.ReducedTensorWords.subword_congr (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n m : ℕ} (x : Fin n → M) (y : Fin m → M) {a a' b : ℕ} (hab : a + b ≤ n) (hab' : a' + b ≤ m) (h : ∀ (j : ℕ) (hj : j < b), x ⟨a + j, ⋯⟩ = y ⟨a' + j, ⋯⟩) : subword R x a b = subword R y a' b

A block of a tensor word depends only on its letters, not on the tuple carrying them nor on where the block sits inside it.

theorem TauCeti.ReducedTensorWords.subword_tail (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {n : ℕ} (z : Fin (n + 1) → M) (a b : ℕ) : subword R (Fin.tail z) a b = subword R z (a + 1) b

A block of the tail of a tuple is the block one position further along the tuple.

theorem TauCeti.ReducedTensorWords.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.Ioo 0 b, subword R x a c ⊗ₜ[R] subword R x (a + c) (b - c)

Deconcatenating a block cuts it at each of its nontrivial internal positions.

theorem TauCeti.ReducedTensorWords.map_deconcatenation_subword (R : Type uR) [CommSemiring R] {M : Type uM} [AddCommMonoid M] [Module R M] {P : Type u_1} {Q : Type u_2} [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] (F : ReducedTensorWords R M →ₗ[R] P) (G : ReducedTensorWords R M →ₗ[R] Q) {n : ℕ} (x : Fin n → M) (a b : ℕ) : (TensorProduct.map F G) ((deconcatenation R M) (subword R x a b)) = ∑ c ∈ Finset.range b, F (subword R x a c) ⊗ₜ[R] G (subword R x (a + c) (b - c))

Mapping both halves of the cuts of a block, written as one sum over the cut position.

noncomputable def TauCeti.ReducedTensorWords.prepend (R : Type uR) (N : Type uN) [CommSemiring R] [AddCommMonoid N] [Module R N] : N →ₗ[R] ReducedTensorWords R N →ₗ[R] ReducedTensorWords R N

Prepend a letter to a reduced tensor word: a and y₁ ⋯ y_k give a y₁ ⋯ y_k.

Equations

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

theorem TauCeti.ReducedTensorWords.prepend_of_tprod {R : Type uR} {N : Type uN} [CommSemiring R] [AddCommMonoid N] [Module R N] (a : N) (k : { n : ℕ // 0 < n }) (y : Fin ↑k → N) : ((prepend R N) a) ((of R N k) ((PiTensorProduct.tprod R) y)) = (of R N ⟨↑k + 1, ⋯⟩) ((PiTensorProduct.tprod R) (Fin.cons a y))

Prepending a letter to a pure tensor word conses it onto the letters.

theorem TauCeti.ReducedTensorWords.prepend_subword {R : Type uR} {N : Type uN} [CommSemiring R] [AddCommMonoid N] [Module R N] {n : ℕ} (z : Fin n → N) {a b : ℕ} (ha : a < n) (hb : 0 < b) : ((prepend R N) (z ⟨a, ha⟩)) (subword R z (a + 1) b) = subword R z a (b + 1)

Prepending the letter at position a to the block that starts right after it extends the block by that letter.

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

Apply a linear map to every letter of a reduced tensor word.

Equations

• TauCeti.ReducedTensorWords.map R f = DirectSum.lmap fun (x : { n : ℕ // 0 < n }) => PiTensorProduct.map fun (x : Fin ↑x) => f

@[simp]

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

Mapping a homogeneous tensor word applies the tensor power of the map in the same length.

@[simp]

theorem TauCeti.ReducedTensorWords.component_map (R : Type uR) [CommSemiring R] {M : Type uM} {N : Type uN} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (n : { n : ℕ // 0 < n }) (x : ReducedTensorWords R M) : (component R N n) ((map R f) x) = (PiTensorProduct.map fun (x : Fin ↑n) => f) ((component R M n) x)

Each length component of a mapped tensor word is the tensor power of the map applied to that component.

theorem TauCeti.ReducedTensorWords.map_of_tprod (R : Type uR) [CommSemiring R] {M : Type uM} {N : Type uN} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (n : { n : ℕ // 0 < n }) (x : Fin ↑n → M) : (map R 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.

theorem TauCeti.ReducedTensorWords.map_subword (R : Type uR) [CommSemiring R] {M : Type uM} {N : Type uN} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) {n : ℕ} (x : Fin n → M) (a b : ℕ) : (map R f) (subword R x a b) = subword R (fun (i : Fin n) => f (x i)) a b

Mapping a block of a tensor word applies the map to each letter in the block.

@[simp]

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

Mapping the identity map over the letters is the identity.

@[simp]

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

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

@[simp]

theorem TauCeti.ReducedTensorWords.map_symm_map (R : Type uR) [CommSemiring R] {M : Type uM} {N : Type uN} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (z : ReducedTensorWords R M) : (map R ↑e.symm) ((map R ↑e) z) = z

Applying a linear equivalence and then its inverse to every letter is the identity.

@[simp]

theorem TauCeti.ReducedTensorWords.map_map_symm (R : Type uR) [CommSemiring R] {M : Type uM} {N : Type uN} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (z : ReducedTensorWords R N) : (map R ↑e) ((map R ↑e.symm) z) = z

Applying the inverse of a linear equivalence and then the equivalence to every letter is the identity.

theorem TauCeti.ReducedTensorWords.map_bijective (R : Type uR) [CommSemiring R] {M : Type uM} {N : Type uN} [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) : Function.Bijective ⇑(map R ↑e)

Applying a linear equivalence to every letter is a bijection of reduced tensor words, with inverse the letterwise inverse equivalence.

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

Reduced deconcatenation is natural with respect to linear maps of the letters.