Special contractions of modules with a differential

A special contraction of a module M with an endomorphism dM onto a module N with an endomorphism dN consists of linear maps incl : N → M and proj : M → N commuting with the endomorphisms, a homotopy h : M → M with

proj ∘ incl = 1, dM h + h dM = 1 - incl ∘ proj,

and the three side conditions h ∘ incl = 0, proj ∘ h = 0, h ∘ h = 0. When dM and dN square to zero this is the classical strong deformation retract of differential modules. The square of dN is in any case the compression of the square of dM to the retract (LinearSpecialContraction.dN_comp_dN), so once dM squares to zero a separate requirement that dN square to zero would be redundant; nothing in the data forces dM itself to square to zero.

TauCeti.SpecialContraction packages the same notion degreewise, for cochain complexes in a preadditive category. The present total-module form is the one homological perturbation theory operates on: the perturbation series inverts an endomorphism of the total module, and the bar constructions it is applied to are modules with an internal grading, not degreewise objects. The orientation of the contracting equation, with 1 - incl ∘ proj on the right, is the one fixed by TauCeti.Contraction; the identity contraction LinearSpecialContraction.refl therefore has zero homotopy.

Main definitions

• TauCeti.LinearSpecialContraction: a special contraction of (M, dM) onto (N, dN).
• TauCeti.LinearSpecialContraction.refl: the identity contraction.

Main results

• TauCeti.LinearSpecialContraction.dN_comp_dN: the square of dN is proj ∘ dM ∘ dM ∘ incl; in particular dN squares to zero when dM does.
• TauCeti.LinearSpecialContraction.isHomogeneous_dN: dN has the degree of dM when the inclusion and projection have degree zero.

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.

structure TauCeti.LinearSpecialContraction {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) : Type (max uM uN)

A special contraction of (M, dM) onto (N, dN): maps incl, proj commuting with the endomorphisms, with proj ∘ incl = 1, and a homotopy h with dM h + h dM = 1 - incl ∘ proj satisfying the side conditions h ∘ incl = 0, proj ∘ h = 0 and h ∘ h = 0. When dM squares to zero (so dN does too, by dN_comp_dN_eq_zero) this is a strong deformation retract of differential modules; for general endomorphisms it is the analogous contraction data.

• incl : N →ₗ[R] M

  the inclusion of the retract

• proj : M →ₗ[R] N

  the projection onto the retract

• homotopy : Module.End R M

  the contracting homotopy

• dM_comp_incl : dM ∘ₗ self.incl = self.incl ∘ₗ dN

  the inclusion commutes with the endomorphisms

• proj_comp_dM : self.proj ∘ₗ dM = dN ∘ₗ self.proj

  the projection commutes with the endomorphisms

• proj_comp_incl : self.proj ∘ₗ self.incl = LinearMap.id

  the projection retracts the inclusion

• dM_comp_homotopy_add_homotopy_comp_dM : dM ∘ₗ self.homotopy + self.homotopy ∘ₗ dM = LinearMap.id - self.incl ∘ₗ self.proj

  dM h + h dM is the complementary idempotent 1 - incl ∘ proj

• homotopy_comp_incl : self.homotopy ∘ₗ self.incl = 0

  the homotopy annihilates the inclusion

• proj_comp_homotopy : self.proj ∘ₗ self.homotopy = 0

  the projection annihilates the homotopy

• homotopy_comp_homotopy : self.homotopy ∘ₗ self.homotopy = 0

  the homotopy squares to zero

theorem TauCeti.LinearSpecialContraction.ext_iff {R : Type uR} {M : Type uM} {N : Type uN} {inst✝ : Semiring R} {inst✝¹ : AddCommGroup M} {inst✝² : Module R M} {inst✝³ : AddCommGroup N} {inst✝⁴ : Module R N} {dM : Module.End R M} {dN : Module.End R N} {x y : LinearSpecialContraction dM dN} : x = y ↔ x.incl = y.incl ∧ x.proj = y.proj ∧ x.homotopy = y.homotopy

theorem TauCeti.LinearSpecialContraction.ext {R : Type uR} {M : Type uM} {N : Type uN} {inst✝ : Semiring R} {inst✝¹ : AddCommGroup M} {inst✝² : Module R M} {inst✝³ : AddCommGroup N} {inst✝⁴ : Module R N} {dM : Module.End R M} {dN : Module.End R N} {x y : LinearSpecialContraction dM dN} (incl : x.incl = y.incl) (proj : x.proj = y.proj) (homotopy : x.homotopy = y.homotopy) : x = y

theorem TauCeti.LinearSpecialContraction.incl_comp_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 : LinearSpecialContraction dM dN) : c.incl ∘ₗ c.proj = LinearMap.id - (dM ∘ₗ c.homotopy + c.homotopy ∘ₗ dM)

The idempotent incl ∘ proj of a special contraction is the complement of dM h + h dM.

Reassociated forms

The defining equations, stated with an arbitrary further factor on the right, so that they can rewrite inside right-associated compositions.

@[simp]

theorem TauCeti.LinearSpecialContraction.proj_comp_incl_assoc {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) {P : Type uP} [AddCommMonoid P] [Module R P] (f : P →ₗ[R] N) : c.proj ∘ₗ c.incl ∘ₗ f = f

@[simp]

theorem TauCeti.LinearSpecialContraction.homotopy_comp_incl_assoc {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) {P : Type uP} [AddCommMonoid P] [Module R P] (f : P →ₗ[R] N) : c.homotopy ∘ₗ c.incl ∘ₗ f = 0

@[simp]

theorem TauCeti.LinearSpecialContraction.proj_comp_homotopy_assoc {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) {P : Type uP} [AddCommMonoid P] [Module R P] (f : P →ₗ[R] M) : c.proj ∘ₗ c.homotopy ∘ₗ f = 0

@[simp]

theorem TauCeti.LinearSpecialContraction.homotopy_comp_homotopy_assoc {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) {P : Type uP} [AddCommMonoid P] [Module R P] (f : P →ₗ[R] M) : c.homotopy ∘ₗ c.homotopy ∘ₗ f = 0

@[simp]

theorem TauCeti.LinearSpecialContraction.dM_comp_incl_assoc {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) {P : Type uP} [AddCommMonoid P] [Module R P] (f : P →ₗ[R] N) : dM ∘ₗ c.incl ∘ₗ f = c.incl ∘ₗ dN ∘ₗ f

@[simp]

theorem TauCeti.LinearSpecialContraction.proj_comp_dM_assoc {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) {P : Type uP} [AddCommMonoid P] [Module R P] (f : P →ₗ[R] M) : c.proj ∘ₗ dM ∘ₗ f = dN ∘ₗ c.proj ∘ₗ f

theorem TauCeti.LinearSpecialContraction.incl_comp_proj_assoc {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) {P : Type uP} [AddCommMonoid P] [Module R P] (f : P →ₗ[R] M) : c.incl ∘ₗ c.proj ∘ₗ f = f - dM ∘ₗ c.homotopy ∘ₗ f - c.homotopy ∘ₗ dM ∘ₗ f

Pointwise forms

The defining equations evaluated on elements.

@[simp]

theorem TauCeti.LinearSpecialContraction.proj_incl_apply {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) (y : N) : c.proj (c.incl y) = y

@[simp]

theorem TauCeti.LinearSpecialContraction.homotopy_incl_apply {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) (y : N) : c.homotopy (c.incl y) = 0

@[simp]

theorem TauCeti.LinearSpecialContraction.proj_homotopy_apply {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) (x : M) : c.proj (c.homotopy x) = 0

@[simp]

theorem TauCeti.LinearSpecialContraction.homotopy_homotopy_apply {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) (x : M) : c.homotopy (c.homotopy x) = 0

@[simp]

theorem TauCeti.LinearSpecialContraction.dM_incl_apply {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) (y : N) : dM (c.incl y) = c.incl (dN y)

@[simp]

theorem TauCeti.LinearSpecialContraction.proj_dM_apply {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) (x : M) : c.proj (dM x) = dN (c.proj x)

theorem TauCeti.LinearSpecialContraction.incl_proj_apply {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) (x : M) : c.incl (c.proj x) = x - dM (c.homotopy x) - c.homotopy (dM x)

The square of the differential of the retract

theorem TauCeti.LinearSpecialContraction.dN_comp_dN {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) : dN ∘ₗ dN = c.proj ∘ₗ dM ∘ₗ dM ∘ₗ c.incl

The square of dN is the compression proj ∘ dM² ∘ incl of the square of dM to the retract.

theorem TauCeti.LinearSpecialContraction.dN_comp_dN_eq_zero {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) (h : dM ∘ₗ dM = 0) : dN ∘ₗ dN = 0

If dM squares to zero, so does the endomorphism of the retract.

theorem TauCeti.LinearSpecialContraction.isHomogeneous_dN {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) {ι : Type u_1} {σM : Type u_2} {σN : Type u_3} [AddMonoid ι] [SetLike σM M] [SetLike σN N] {𝒜 : ι → σM} {ℬ : ι → σN} {q : ι} (hdM : LinearMap.IsHomogeneous dM 𝒜 𝒜 q) (hincl : LinearMap.IsHomogeneous c.incl ℬ 𝒜 0) (hproj : LinearMap.IsHomogeneous c.proj 𝒜 ℬ 0) : LinearMap.IsHomogeneous dN ℬ ℬ q

The endomorphism of the retract has the degree of dM when the inclusion and projection have degree zero, since it is the compression proj ∘ dM ∘ incl.

def TauCeti.LinearSpecialContraction.refl {R : Type uR} {M : Type uM} [Semiring R] [AddCommGroup M] [Module R M] (dM : Module.End R M) : LinearSpecialContraction dM dM

Every module with an endomorphism is a special contraction of itself, with zero homotopy. This pins the orientation of the contracting equation: it has 1 - incl ∘ proj on the right.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LinearSpecialContraction.refl_incl {R : Type uR} {M : Type uM} [Semiring R] [AddCommGroup M] [Module R M] (dM : Module.End R M) : (refl dM).incl = LinearMap.id

The identity contraction has the identity as inclusion.

@[simp]

theorem TauCeti.LinearSpecialContraction.refl_proj {R : Type uR} {M : Type uM} [Semiring R] [AddCommGroup M] [Module R M] (dM : Module.End R M) : (refl dM).proj = LinearMap.id

The identity contraction has the identity as projection.

@[simp]

theorem TauCeti.LinearSpecialContraction.refl_homotopy {R : Type uR} {M : Type uM} [Semiring R] [AddCommGroup M] [Module R M] (dM : Module.End R M) : (refl dM).homotopy = 0

The identity contraction has zero homotopy.