The conilpotence filtration of reduced tensor words

The reduced tensor coalgebra is filtered by tensor length, and reduced deconcatenation strictly decreases that length: a word of length at most n + 1 is cut into two words each of length at most n. This length bound is the inductive step behind conilpotence, which asserts that a high enough iterate of the reduced coproduct annihilates every element.

The filtration is exhaustive and starts at the zero submodule, since the empty word is not a reduced tensor word.

Main definitions

• TauCeti.ReducedTensorWords.filtration: the submodule generated by the tensor words of length at most n.

Main results

• TauCeti.ReducedTensorWords.iSup_filtration_eq_top and TauCeti.ReducedTensorWords.exists_mem_filtration: the filtration is exhaustive.
• TauCeti.ReducedTensorWords.exists_pow_apply_eq_zero_of_filtration_lowering: a map lowering tensor length is locally nilpotent, also after composition with a length-preserving map.
• TauCeti.ReducedTensorWords.ofLetter_mem_filtration and TauCeti.ReducedTensorWords.prepend_mem_filtration: a letter has length one, and prepending a letter raises the length bound by one.
• TauCeti.ReducedTensorWords.map_deconcatenation_filtration_succ_le: deconcatenating a word of length at most n + 1 produces a sum of tensors of two words of length at most n.

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

The n-th step of the conilpotence filtration: the submodule generated by the tensor words of length at most n.

Equations

• TauCeti.ReducedTensorWords.filtration R M n = ⨆ (k : { k : ℕ // 0 < k }), ⨆ (_ : ↑k ≤ n), (TauCeti.ReducedTensorWords.of R M k).range

theorem TauCeti.ReducedTensorWords.of_mem_filtration (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {k : { k : ℕ // 0 < k }} {n : ℕ} (hk : ↑k ≤ n) (x : TensorPower R (↑k) M) : (of R M k) x ∈ filtration R M n

A tensor word of length at most n lies in the n-th step of the filtration.

theorem TauCeti.ReducedTensorWords.filtration_le_iff (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {p : Submodule R (ReducedTensorWords R M)} : filtration R M n ≤ p ↔ ∀ (k : { k : ℕ // 0 < k }), ↑k ≤ n → (of R M k).range ≤ p

To prove that the n-th filtration step lies in a submodule, it suffices to check the generating tensor powers of length at most n.

theorem TauCeti.ReducedTensorWords.filtration_monotone (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : Monotone (filtration R M)

The conilpotence filtration is increasing.

@[simp]

theorem TauCeti.ReducedTensorWords.filtration_zero (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : filtration R M 0 = ⊥

A reduced tensor word has positive length, so the filtration starts at zero.

theorem TauCeti.ReducedTensorWords.iSup_filtration_eq_top (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] : ⨆ (n : ℕ), filtration R M n = ⊤

The conilpotence filtration is exhaustive.

theorem TauCeti.ReducedTensorWords.exists_mem_filtration (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (z : ReducedTensorWords R M) : ∃ (n : ℕ), z ∈ filtration R M n

Every reduced tensor word has bounded length: it lies in some step of the filtration.

theorem TauCeti.ReducedTensorWords.exists_pow_apply_eq_zero_of_filtration_lowering (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.End R (ReducedTensorWords R M)) (hf : ∀ (n : ℕ), Submodule.map f (filtration R M (n + 1)) ≤ filtration R M n) (z : ReducedTensorWords R M) : ∃ (n : ℕ), (f ^ n) z = 0

A map strictly lowering the tensor-length filtration is locally nilpotent.

theorem TauCeti.ReducedTensorWords.exists_pow_comp_apply_eq_zero_of_filtration_lowering (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (f h : Module.End R (ReducedTensorWords R M)) (hf : ∀ (n : ℕ), Submodule.map f (filtration R M (n + 1)) ≤ filtration R M n) (hh : ∀ (n : ℕ), Submodule.map h (filtration R M n) ≤ filtration R M n) (z : ReducedTensorWords R M) : ∃ (n : ℕ), ((f ∘ₗ h) ^ n) z = 0

Composing a strictly length-lowering map with a length-preserving map remains locally nilpotent.

theorem TauCeti.ReducedTensorWords.subword_mem_filtration (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] {l : ℕ} (x : Fin l → M) (a : ℕ) {b n : ℕ} (hb : b ≤ n) : subword R x a b ∈ filtration R M n

A block of length at most n lies in the n-th step of the filtration.

theorem TauCeti.ReducedTensorWords.ofLetter_mem_filtration (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) : (ofLetter R M) a ∈ filtration R M 1

A single letter is a word of length at most one.

theorem TauCeti.ReducedTensorWords.prepend_mem_filtration (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : M) {n : ℕ} {z : ReducedTensorWords R M} (hz : z ∈ filtration R M n) : ((prepend R M) a) z ∈ filtration R M (n + 1)

Prepending a letter to a word of length at most n gives a word of length at most n + 1.

theorem TauCeti.ReducedTensorWords.map_deconcatenation_filtration_succ_le (R : Type uR) (M : Type uM) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : Submodule.map (deconcatenation R M) (filtration R M (n + 1)) ≤ (TensorProduct.mapIncl (filtration R M n) (filtration R M n)).range

Reduced deconcatenation strictly decreases tensor length: a word of length at most n + 1 is sent into the image of filtration n ⊗ filtration n. This is the length-lowering step behind the conilpotence of the reduced tensor coalgebra.