Tensor length and the tensor-trick homotopy #
The tensor-trick homotopy acts on one letter at a time and therefore preserves tensor length. Together with the length-lowering higher bar differential, this makes their composite locally nilpotent, the hypothesis of the basic perturbation lemma.
The construction follows Gugenheim--Lambe--Stasheff, Perturbation theory in differential homological algebra II.
theorem
TauCeti.LinearSpecialContraction.reducedTensorWordsHomotopy_filtration
{R : Type uR}
{M : Type uM}
{N : Type uN}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{dM : Module.End R M}
{dN : Module.End R N}
(c : LinearSpecialContraction dM dN)
(G : InternalGrading R M)
(n : ℕ)
:
The tensor-trick homotopy preserves the filtration by tensor length.