The perturbed tensor-trick homotopy #
The coalgebra perturbation lemma preserves not only the inclusion and projection, but also the
coderivation identity of the homotopy. If i', p', h' are the perturbed tensor-trick maps,
then h' is an odd coderivation along id and i' p'. This supplies the bar homotopy needed to
compare an A-infinity algebra with its transferred structure.
The perturbation need not lower tensor length here: invertibility of 1 + δ h suffices.
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.
- J. Huebschmann and T. Kadeishvili, Small models for chain algebras, Mathematische Zeitschrift 207 (1991), 245--280.
theorem
TauCeti.LinearSpecialContraction.isGradedCoderivationAlong_reducedTensorWords_perturb_homotopy
{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}
{H : InternalGrading R N}
(hdM : LinearMap.IsHomogeneous dM G.piece G.piece 1)
(hh : LinearMap.IsHomogeneous c.homotopy G.piece G.piece (-1))
(hincl : LinearMap.IsHomogeneous c.incl H.piece G.piece 0)
(hproj : LinearMap.IsHomogeneous c.proj G.piece H.piece 0)
{δ : Module.End R (ReducedTensorWords R M)}
(hsq :
(ReducedTensorWords.gradedCoderiv G (dM ∘ₗ ReducedTensorWords.letter R M) 1 + δ) ∘ₗ (ReducedTensorWords.gradedCoderiv G (dM ∘ₗ ReducedTensorWords.letter R M) 1 + δ) = ReducedTensorWords.gradedCoderiv G (dM ∘ₗ ReducedTensorWords.letter R M) 1 ∘ₗ ReducedTensorWords.gradedCoderiv G (dM ∘ₗ ReducedTensorWords.letter R M) 1)
(hU : IsUnit (1 + δ * (c.reducedTensorWords G H hdM hh hincl hproj).homotopy))
(hδ : ReducedTensorWords.IsGradedCoderivation G 1 δ)
:
ReducedTensorWords.IsGradedCoderivationAlong G 1 LinearMap.id
(((c.reducedTensorWords G H hdM hh hincl hproj).perturb δ hsq hU).incl ∘ₗ ((c.reducedTensorWords G H hdM hh hincl hproj).perturb δ hsq hU).proj)
((c.reducedTensorWords G H hdM hh hincl hproj).perturb δ hsq hU).homotopy
The perturbed tensor-trick homotopy is an odd coderivation along id and the perturbed
inclusion followed by the perturbed projection. No length-lowering hypothesis is needed.