Prepending a letter to a possibly empty tensor word

TauCeti.TensorWords.prepend sends a letter a and a tensor word y₁ ⋯ y_k, the empty word included, to the nonempty word a y₁ ⋯ y_k. Its uncurried form is the concatenation map M ⊗ Tᶜ(M) → ReducedTensorWords R M onto the reduced tensor words. Through it, the cofree right bar comodule sA ⊗ Tᶜ(sA) of an A∞ algebra A, regarded as a right module over itself, is compared with the reduced bar construction ReducedTensorWords R A of A.

On positive-length words it is TauCeti.ReducedTensorWords.prepend, and on the empty word it is the single letter. The remaining lemmas evaluate it on blocks of a tuple, as subwords or splices, which is the form in which coderivations are expanded.

Main definitions

• TauCeti.TensorWords.prepend: prepend a letter to a tensor word.

Main results

• TauCeti.TensorWords.prepend_of_tprod: prepending conses the letter onto a pure tensor word.
• TauCeti.TensorWords.prepend_one and TauCeti.TensorWords.prepend_reducedInclusion: the empty and the positive-length cases.
• TauCeti.TensorWords.prepend_subword and TauCeti.TensorWords.prepend_subword_eq_splice: prepending to a block of a tuple.
• TauCeti.TensorWords.prepend_mem_gradedPiece and TauCeti.TensorWords.isHomogeneous_lift_prepend: prepending adds total letter degrees.
• TauCeti.TensorWords.subword_tail: blocks of the tail of a tuple.

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, Section 4.

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

Prepend a letter to a tensor word: a and y₁ ⋯ y_k give the nonempty word a y₁ ⋯ y_k. Uncurried, this is the concatenation map M ⊗ Tᶜ(M) → ReducedTensorWords R M.

Equations

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

theorem TauCeti.TensorWords.subword_tail {R : Type uR} {M : Type uM} [CommSemiring R] [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.TensorWords.prepend_of_tprod {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) (k : ℕ) (y : Fin k → M) : ((prepend R M) a) ((of R M k) ((PiTensorProduct.tprod R) y)) = (ReducedTensorWords.of R M ⟨k + 1, ⋯⟩) ((PiTensorProduct.tprod R) (Fin.cons a y))

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

@[simp]

theorem TauCeti.TensorWords.prepend_one {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) : ((prepend R M) a) 1 = (ReducedTensorWords.ofLetter R M) a

Prepending a letter to the empty word gives that letter as a word of length one.

@[simp]

theorem TauCeti.TensorWords.prepend_reducedInclusion {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) (w : ReducedTensorWords R M) : ((prepend R M) a) ((reducedInclusion R M) w) = ((ReducedTensorWords.prepend R M) a) w

On words of positive length, prepending agrees with prepending in the reduced tensor words.

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

Prepending the letter at position a to the (possibly empty) block after it extends the block by that letter.

theorem TauCeti.TensorWords.prepend_subword_eq_splice {R : Type uR} {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (z : Fin n → M) {a b d : ℕ} (hd : 0 < d) (hdb : d ≤ b) (hab : a + b ≤ n) (e : M) : ((prepend R M) e) (subword R z (a + d) (b - d)) = ReducedTensorWords.splice R z a b 0 d e

Prepending a letter e to the block that follows the first d letters of a block replaces those d letters by e.

theorem TauCeti.TensorWords.prepend_mem_gradedPiece {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {G : InternalGrading R M} {p D : ℤ} {a : M} (ha : a ∈ G.piece p) {w : TensorWords R M} (hw : w ∈ gradedPiece G D) : ((prepend R M) a) w ∈ ReducedTensorWords.gradedPiece G (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.TensorWords.isHomogeneous_lift_prepend {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (G : InternalGrading R M) : LinearMap.IsHomogeneous (TensorProduct.lift (prepend R M)) (G.tensorProduct (grading G)).piece (ReducedTensorWords.gradedPiece G) 0

Uncurried prepending preserves total degrees: it is homogeneous of degree zero from the tensor-product grading of M ⊗ Tᶜ(M) to the total-letter-degree grading of the reduced words.