Collapsing a block of a tensor word to a single letter

For an R-module M, TauCeti.ReducedTensorWords.splice x a b p d e is the tensor word obtained from the block x a ⋯ x (a + b - 1) by deleting its d letters at relative offset p and putting the single letter e in their place. It is the shape of every summand of a coderivation of the reduced tensor coalgebra, whose Taylor expansion replaces one block of letters by the value of a single operation on that block.

The main computation here is TauCeti.ReducedTensorWords.deconcatenation_splice: a cut of a spliced word falls either weakly to the left of the new letter, leaving a plain block on the left and a spliced word on the right, or strictly to its right, leaving a spliced word on the left and a plain block on the right. No cut splits the new letter, a letter having no internal position. Written this way both halves are again of the two shapes subword and splice, which is what makes the coderivation identity an equality of two sums over the same pairs of a cut position and a collapsed block.

Main definitions

• TauCeti.ReducedTensorWords.splice: a block of a tensor word with one of its subblocks collapsed to a single letter.

Main results

• TauCeti.ReducedTensorWords.splice_congr: a spliced word depends only on the letters spliced.
• TauCeti.ReducedTensorWords.map_splice: mapping a spliced word maps each of its letters.
• TauCeti.ReducedTensorWords.deconcatenation_splice: reduced deconcatenation of a spliced word.
• TauCeti.ReducedTensorWords.prepend_splice: prepending the first letter of a tuple commutes with splicing a block of the rest.

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.splice (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) (a b p d : ℕ) (e : M) : ReducedTensorWords R M

The block x a ⊗ ⋯ ⊗ x (a + b - 1) with its d letters at relative offset p replaced by the single letter e, a tensor word of length b + 1 - d.

It is zero unless the collapsed block is nonempty and fits inside the block being spliced, which fits inside x; the intended range of the definition is 0 < d, p + d ≤ b and a + b ≤ n.

Equations

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

theorem TauCeti.ReducedTensorWords.splice_eq_of_tprod (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b p d : ℕ} (e : M) (hd : 0 < d) (hpd : p + d ≤ b) (hab : a + b ≤ n) : splice R x a b p d e = (of R M ⟨b + 1 - d, ⋯⟩) ((PiTensorProduct.tprod R) fun (j : Fin (b + 1 - d)) => if x_1 : ↑j < p then x ⟨a + ↑j, ⋯⟩ else if x : ↑j = p then e else x ⟨a + (↑j + d - 1), ⋯⟩)

On its intended range, a spliced word is the pure tensor of its letters: the letters of the block before the collapsed subblock, then the new letter, then the letters after it.

@[simp]

theorem TauCeti.ReducedTensorWords.splice_zero_length (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) (a b p : ℕ) (e : M) : splice R x a b p 0 e = 0

Collapsing an empty subblock is zero: a letter is never produced out of nothing.

@[simp]

theorem TauCeti.ReducedTensorWords.splice_eq_zero_of_block_lt_add (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b p d : ℕ} (e : M) (hpd : b < p + d) : splice R x a b p d e = 0

A collapsed subblock running past the end of the spliced block is zero: the length b of that block is smaller than the end p + d of the subblock.

@[simp]

theorem TauCeti.ReducedTensorWords.splice_eq_zero_of_length_lt_add (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b p d : ℕ} (e : M) (hab : n < a + b) : splice R x a b p d e = 0

A spliced block running past the end of the tuple is zero: the length n of the tuple is smaller than the end a + b of the block.

theorem TauCeti.ReducedTensorWords.splice_eq_zero (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b p d : ℕ} (e : M) (h : ¬(0 < d ∧ p + d ≤ b ∧ a + b ≤ n)) : splice R x a b p d e = 0

A spliced word is zero outside the intended range of the definition.

theorem TauCeti.ReducedTensorWords.splice_eq_zero_of_not_fits (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) {a b p d : ℕ} (e : M) (h : ¬(0 < d ∧ p + d ≤ b)) : splice R x a b p d e = 0

A spliced word vanishes when the collapsed block does not fit into the block being spliced into: either the collapsed block is empty, or it overruns that block.

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

A spliced word depends only on the letters of the block it splices, not on the tuple carrying them nor on the position of the block in it.

@[simp]

theorem TauCeti.ReducedTensorWords.splice_zero (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) (a b p d : ℕ) : splice R x a b p d 0 = 0

Splicing in the zero letter gives the zero word.

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

Mapping a spliced tensor word applies the map to the untouched letters and the replacement letter.

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

Reduced deconcatenation of a spliced word. A cut never splits the new letter, so it falls either weakly to its left, leaving a plain block and a spliced word, or strictly to its right, leaving a spliced word and a plain block. Both sums range over the cut position measured in the original block, and their summands vanish outside the positions that really occur; that is what makes the identity hold for a degenerate collapsed block too, both sides then being zero.

theorem TauCeti.ReducedTensorWords.prepend_splice (R : Type uR) {M : Type uM} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (y : Fin (n + 1) → M) (p d : ℕ) (e : M) : ((prepend R M) (y 0)) (splice R (Fin.tail y) 0 n p d e) = splice R y 0 (n + 1) (p + 1) d e

Prepending the first letter of a tuple to a splice of the remaining letters is the splice of the whole tuple at the next position.