Normalization of contractions on total modules

LinearContraction packages weak contraction data: its inclusion and projection are chain maps, the projection retracts the inclusion, and its homotopy contracts the complementary idempotent. No side conditions are required of the homotopy. Normalization turns this data into the LinearSpecialContraction consumed by homological perturbation.

For a square-zero differential, LinearContraction.normalize keeps the inclusion and projection and supplies all three side conditions required by LinearSpecialContraction. Write ψ = 1 - incl ∘ proj and k = ψ ∘ homotopy ∘ ψ; the normalized homotopy is k ∘ dM ∘ k. Normalization preserves the degrees of the maps, so its output can be used by the graded tensor trick and homological transfer over an arbitrary ground ring.

This is the total-module counterpart of TauCeti.Contraction.normalize, which works with cochains of cochain complexes. Here the data and normalization require no grading at all; homogeneity is proved separately when gradings are supplied.

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.
• M. Crainic, On the perturbation lemma, and deformations, Section 2.

def TauCeti.LinearContraction.normalize {R : Type uR} {M : Type uM} {N : Type uN} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {dM : Module.End R M} {dN : Module.End R N} (c : LinearContraction dM dN) (hd : dM ∘ₗ dM = 0) : LinearSpecialContraction dM dN

Normalize a contraction of differential modules, retaining its inclusion and projection. The homotopy is (ψ h ψ) dM (ψ h ψ), where ψ = 1 - incl ∘ proj.

@[simp]

theorem TauCeti.LinearContraction.normalize_incl {R : Type uR} {M : Type uM} {N : Type uN} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {dM : Module.End R M} {dN : Module.End R N} (c : LinearContraction dM dN) (hd : dM ∘ₗ dM = 0) : (c.normalize hd).incl = c.incl

@[simp]

theorem TauCeti.LinearContraction.normalize_proj {R : Type uR} {M : Type uM} {N : Type uN} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {dM : Module.End R M} {dN : Module.End R N} (c : LinearContraction dM dN) (hd : dM ∘ₗ dM = 0) : (c.normalize hd).proj = c.proj

theorem TauCeti.LinearContraction.normalize_homotopy {R : Type uR} {M : Type uM} {N : Type uN} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {dM : Module.End R M} {dN : Module.End R N} (c : LinearContraction dM dN) (hd : dM ∘ₗ dM = 0) : (c.normalize hd).homotopy = ((LinearMap.id - c.incl ∘ₗ c.proj) ∘ₗ c.homotopy ∘ₗ (LinearMap.id - c.incl ∘ₗ c.proj)) ∘ₗ dM ∘ₗ (LinearMap.id - c.incl ∘ₗ c.proj) ∘ₗ c.homotopy ∘ₗ (LinearMap.id - c.incl ∘ₗ c.proj)

The explicit homotopy supplied by normalization.

theorem TauCeti.LinearContraction.isHomogeneous_normalize_homotopy {R : Type uR} {M : Type uM} {N : Type uN} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {dM : Module.End R M} {dN : Module.End R N} (c : LinearContraction dM dN) (hd : dM ∘ₗ dM = 0) {ι : Type u_1} {σM : Type u_2} {σN : Type u_3} [AddGroup ι] [SetLike σM M] [AddSubgroupClass σM M] [SetLike σN N] {𝒜 : ι → σM} {ℬ : ι → σN} {q : ι} (hdM : LinearMap.IsHomogeneous dM 𝒜 𝒜 q) (hi : LinearMap.IsHomogeneous c.incl ℬ 𝒜 0) (hp : LinearMap.IsHomogeneous c.proj 𝒜 ℬ 0) (hh : LinearMap.IsHomogeneous c.homotopy 𝒜 𝒜 (-q)) : LinearMap.IsHomogeneous (c.normalize hd).homotopy 𝒜 𝒜 (-q)

For a differential of degree q, normalization preserves homotopy degree -q.

@[simp]

theorem TauCeti.LinearSpecialContraction.normalize_toLinearContraction {R : Type uR} {M : Type uM} {N : Type uN} [Semiring 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) (hd : dM ∘ₗ dM = 0) : c.normalize hd = c

Normalization leaves an already special contraction unchanged.