Naturality of the tensor-trick homotopy #
The tensor trick sends compatible degree-zero maps between graded special contractions to compatible maps on reduced tensor words. The homotopy identity is the nontrivial part: each single-slot homotopy commutes with the letterwise map, including the Koszul twists before that slot and the inclusion-projection composite after it.
References #
- V. K. A. M. Gugenheim, L. A. Lambe, and J. D. Stasheff, Perturbation theory in differential homological algebra II, Illinois Journal of Mathematics 35 (1991), 357--373.
theorem
TauCeti.LinearSpecialContraction.reducedTensorWordsHomotopy_naturality
{R : Type uR}
[CommRing R]
{M : Type uM}
{N : Type uN}
{M' : Type uM'}
{N' : Type uN'}
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[AddCommGroup M']
[Module R M']
[AddCommGroup N']
[Module R N']
{dM : Module.End R M}
{dN : Module.End R N}
{dM' : Module.End R M'}
{dN' : Module.End R N'}
(c : LinearSpecialContraction dM dN)
(c' : LinearSpecialContraction dM' dN')
{G : InternalGrading R M}
{G' : InternalGrading R M'}
(f : M →ₗ[R] M')
(g : N →ₗ[R] N')
(hf : LinearMap.IsHomogeneous f G.piece G'.piece 0)
(hi : f ∘ₗ c.incl = c'.incl ∘ₗ g)
(hp : g ∘ₗ c.proj = c'.proj ∘ₗ f)
(hh : f ∘ₗ c.homotopy = c'.homotopy ∘ₗ f)
:
The reduced tensor-word homotopies commute with the letterwise map induced by a homogeneous degree-zero map between compatible contractions.