Concatenation of tensor words

For a module X, TauCeti.TensorWords.tmulConcat sends x : X to the linear map A ⊗ Tᶜ(A) → X ⊗ Tᶜ(A), y ⊗ w ↦ x ⊗ y w, where y w is the word w with the letter y prepended. On cofree bar comodules X ⊗ Tᶜ(A) it is the map through which representable A∞ modules are compared with the underlying complex of a module.

TauCeti.TensorWords.concatLetter concatenates two words around a letter, w ⊗ x ⊗ v ↦ w x v, using the multiplication of the tensor algebra. It maps the cofree bar bicomodule Tᶜ(A) ⊗ A ⊗ Tᶜ(A) to the nonempty words, and it is the map through which the diagonal A∞ bimodule of an A∞ algebra is compared with its bar construction. Its evaluations on blocks of one ambient tuple are recorded in the subword and splice vocabulary of the bar construction.

Main definitions

• TauCeti.TensorWords.tmulConcat: concatenation behind a fixed first factor.
• TauCeti.TensorWords.concatLetter: concatenation of two words around a letter.

Main results

• TauCeti.TensorWords.cofreeLift_comp_tmulConcat: the cofree lift of a linear map after concatenation splits into the cut before the first letter and the cofree lift of the concatenated map.
• TauCeti.TensorWords.isHomogeneous_tmulConcat: concatenation behind an element of degree q raises the total degree by q.
• TauCeti.TensorWords.concatLetter_of_tprod: concatenation around a letter appends the letter tuples.
• TauCeti.TensorWords.concatLetter_subword, TauCeti.TensorWords.concatLetter_eq_splice, TauCeti.TensorWords.concatLetter_reducedInclusion_splice_left and TauCeti.TensorWords.concatLetter_reducedInclusion_splice_right: concatenating consecutive blocks of a tuple, one of which may carry a collapsed subblock, gives the corresponding block or spliced block.
• TauCeti.TensorWords.isHomogeneous_concatLetter: concatenation around a letter preserves total degrees.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 4.

noncomputable def TauCeti.TensorWords.tmulConcat (R : Type uR) (A : Type uA) [CommRing R] [AddCommGroup A] [Module R A] (X : Type uX) [AddCommGroup X] [Module R X] : X →ₗ[R] TensorProduct R A (TensorWords R A) →ₗ[R] TensorProduct R X (TensorWords R A)

Concatenation after a fixed first factor: x sends y ⊗ w to x ⊗ y w, where y w is the word w with the letter y prepended.

theorem TauCeti.TensorWords.tmulConcat_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {X : Type uX} [AddCommGroup X] [Module R X] (x : X) (z : TensorProduct R A (TensorWords R A)) : ((tmulConcat R A X) x) z = x ⊗ₜ[R] (reducedInclusion R A) ((TensorProduct.lift (prepend R A)) z)

Concatenation behind x applies prepending, followed by the inclusion of the nonempty words, behind x.

@[simp]

theorem TauCeti.TensorWords.tmulConcat_tmul {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {X : Type uX} [AddCommGroup X] [Module R X] (x : X) (y : A) (w : TensorWords R A) : ((tmulConcat R A X) x) (y ⊗ₜ[R] w) = x ⊗ₜ[R] (reducedInclusion R A) (((prepend R A) y) w)

Concatenation behind x sends y ⊗ w to x ⊗ y w.

theorem TauCeti.TensorWords.cofreeLift_comp_tmulConcat {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {X : Type uX} [AddCommGroup X] [Module R X] {N : Type uN} [AddCommGroup N] [Module R N] (φ : TensorProduct R X (TensorWords R A) →ₗ[R] N) (z : X) : (Comodule.Hom.cofreeLift φ).toLinearMap ∘ₗ (tmulConcat R A X) z = (tmulConcat R A N) (φ (z ⊗ₜ[R] 1)) + (Comodule.Hom.cofreeLift (φ ∘ₗ (tmulConcat R A X) z)).toLinearMap

The cofree lift of φ after concatenation behind z: the cut before the first letter of the concatenated word gives φ (z ⊗ 1) in front of the whole word, and every other cut falls inside the concatenated word.

theorem TauCeti.TensorWords.isHomogeneous_tmulConcat {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {X : Type uX} [AddCommGroup X] [Module R X] (G : InternalGrading R A ℤ) (H : InternalGrading R X ℤ) {q : ℤ} {x : X} (hx : x ∈ H.piece ℤ q) : LinearMap.IsHomogeneous ((tmulConcat R A X) x) ((G.tensorProduct (grading G)).piece ℤ) ((H.tensorProduct (grading G)).piece ℤ) q

Concatenation behind an element of degree q raises the total degree by q.

noncomputable def TauCeti.TensorWords.concatLetter (R : Type uR) (A : Type uA) [CommSemiring R] [AddCommMonoid A] [Module R A] : TensorProduct R (TensorProduct R (TensorWords R A) A) (TensorWords R A) →ₗ[R] ReducedTensorWords R A

Concatenation of two words around a letter: w ⊗ x ⊗ v ↦ w x v, computed with the multiplication of the tensor algebra. The result is a nonempty word.

theorem TauCeti.TensorWords.concatLetter_tmul {R : Type uR} {A : Type uA} [CommSemiring R] [AddCommMonoid A] [Module R A] (w : TensorWords R A) (x : A) (v : TensorWords R A) : (concatLetter R A) (w ⊗ₜ[R] x ⊗ₜ[R] v) = (reducedProjection R A) (w * (reducedInclusion R A) (((prepend R A) x) v))

Concatenation around a letter multiplies the first word with the second word prepended by the letter.

theorem TauCeti.TensorWords.concatLetter_of_tprod {R : Type uR} {A : Type uA} [CommSemiring R] [AddCommMonoid A] [Module R A] {l n : ℕ} (w : Fin l → A) (x : A) (v : Fin n → A) : (concatLetter R A) ((of R A l) ((PiTensorProduct.tprod R) w) ⊗ₜ[R] x ⊗ₜ[R] (of R A n) ((PiTensorProduct.tprod R) v)) = (ReducedTensorWords.of R A ⟨l + (n + 1), ⋯⟩) ((PiTensorProduct.tprod R) (Fin.append w (Fin.cons x v)))

Concatenation around a letter appends the letter tuples: w ⊗ x ⊗ v becomes the word of Fin.append w (Fin.cons x v).

theorem TauCeti.TensorWords.concatLetter_subword {R : Type uR} {A : Type uA} [CommSemiring R] [AddCommMonoid A] [Module R A] {N : ℕ} (y : Fin N → A) {a l k : ℕ} (h : a + l + 1 + k ≤ N) : (concatLetter R A) (subword R y a l ⊗ₜ[R] y ⟨a + l, ⋯⟩ ⊗ₜ[R] subword R y (a + l + 1) k) = ReducedTensorWords.subword R y a (l + 1 + k)

Concatenating the block of length l at a, the letter after it, and the block of length k after that letter gives the block of length l + 1 + k at a.

theorem TauCeti.TensorWords.concatLetter_eq_splice {R : Type uR} {A : Type uA} [CommSemiring R] [AddCommMonoid A] [Module R A] {N : ℕ} (y : Fin N → A) {a j d k : ℕ} (e : A) (hd : 0 < d) (h : a + j + d + k ≤ N) : (concatLetter R A) (subword R y a j ⊗ₜ[R] e ⊗ₜ[R] subword R y (a + j + d) k) = ReducedTensorWords.splice R y a (j + d + k) j d e

Concatenating the block of length j at a, a letter e, and the block of length k that starts d letters after the first block ends replaces those d letters by e.

theorem TauCeti.TensorWords.concatLetter_reducedInclusion_splice_left {R : Type uR} {A : Type uA} [CommSemiring R] [AddCommMonoid A] [Module R A] {N : ℕ} (y : Fin N → A) {a l p d k : ℕ} (e : A) (hpd : p + d ≤ l) (h : a + l + 1 + k ≤ N) : (concatLetter R A) ((reducedInclusion R A) (ReducedTensorWords.splice R y a l p d e) ⊗ₜ[R] y ⟨a + l, ⋯⟩ ⊗ₜ[R] subword R y (a + l + 1) k) = ReducedTensorWords.splice R y a (l + 1 + k) p d e

Concatenating a spliced block of length l at a, the letter after it, and the block of length k after that letter gives the spliced block of length l + 1 + k at a, provided the collapsed subblock lies inside the first block.

theorem TauCeti.TensorWords.concatLetter_reducedInclusion_splice_right {R : Type uR} {A : Type uA} [CommSemiring R] [AddCommMonoid A] [Module R A] {N : ℕ} (y : Fin N → A) {a l p d k : ℕ} (e : A) (h : a + l + 1 + k ≤ N) : (concatLetter R A) (subword R y a l ⊗ₜ[R] y ⟨a + l, ⋯⟩ ⊗ₜ[R] (reducedInclusion R A) (ReducedTensorWords.splice R y (a + l + 1) k p d e)) = ReducedTensorWords.splice R y a (l + 1 + k) (l + 1 + p) d e

Concatenating the block of length l at a, the letter after it, and a spliced block of length k after that letter gives the spliced block of length l + 1 + k at a, with the collapsed subblock moved l + 1 positions to the right.

theorem TauCeti.TensorWords.concatLetter_mem_gradedPiece {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {G : InternalGrading R A ℤ} {D p E : ℤ} {w v : TensorWords R A} {x : A} (hw : w ∈ gradedPiece G D) (hx : x ∈ G.piece ℤ p) (hv : v ∈ gradedPiece G E) : (concatLetter R A) (w ⊗ₜ[R] x ⊗ₜ[R] v) ∈ ReducedTensorWords.gradedPiece G (D + p + E)

Concatenating words of total degrees D and E around a letter of degree p gives a word of total degree D + p + E.

theorem TauCeti.TensorWords.isHomogeneous_concatLetter {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (G : InternalGrading R A ℤ) : LinearMap.IsHomogeneous (concatLetter R A) ((((grading G).tensorProduct G).tensorProduct (grading G)).piece ℤ) (ReducedTensorWords.gradedPiece G) 0

Concatenation around a letter preserves total degrees: it is homogeneous of degree zero from the tensor-product grading of Tᶜ(A) ⊗ A ⊗ Tᶜ(A) to the total-letter-degree grading of the reduced words.