Contractions of modules with a differential

LinearContraction packages contraction data without side conditions on the homotopy. LinearSpecialContraction.toLinearContraction forgets the side conditions of a special contraction. Normalization of weak contractions is developed in TauCeti.Algebra.Homology.Contraction.Linear.Normalization.

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 (LinearContraction.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.LinearContraction: a contraction of (M, dM) onto (N, dN) without side conditions.
• TauCeti.LinearSpecialContraction: a special contraction of (M, dM) onto (N, dN).
• TauCeti.LinearSpecialContraction.refl: the identity contraction.

Main results

• TauCeti.LinearContraction.dN_comp_dN: the square of dN is proj ∘ dM ∘ dM ∘ incl; in particular dN squares to zero when dM does.
• TauCeti.LinearContraction.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.LinearContraction {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 contraction of modules with endomorphisms, without side conditions on its homotopy. For square-zero endomorphisms this is a deformation retract of differential modules.

• 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 is a chain map.

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

  The projection is a chain map.

• 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

  The homotopy contracts the complementary idempotent.

theorem TauCeti.LinearContraction.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 : LinearContraction dM dN} : x = y ↔ x.incl = y.incl ∧ x.proj = y.proj ∧ x.homotopy = y.homotopy

theorem TauCeti.LinearContraction.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 : LinearContraction dM dN} (incl : x.incl = y.incl) (proj : x.proj = y.proj) (homotopy : x.homotopy = y.homotopy) : x = y

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem TauCeti.LinearContraction.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 : LinearContraction 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

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

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

theorem TauCeti.LinearContraction.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 : LinearContraction 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.

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) extends TauCeti.LinearContraction dM dN : 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
• proj : M →ₗ[R] N
• homotopy : Module.End R M
• dM_comp_incl : dM ∘ₗ self.incl = self.incl ∘ₗ dN
• proj_comp_dM : self.proj ∘ₗ dM = dN ∘ₗ self.proj
• proj_comp_incl : self.proj ∘ₗ self.incl = LinearMap.id
• dM_comp_homotopy_add_homotopy_comp_dM : dM ∘ₗ self.homotopy + self.homotopy ∘ₗ dM = LinearMap.id - self.incl ∘ₗ self.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

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.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

Pointwise forms

The defining equations evaluated on elements.

@[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.homotopy_comp_dM_comp_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 : LinearSpecialContraction dM dN) : c.homotopy ∘ₗ dM ∘ₗ c.homotopy = c.homotopy

In a special contraction, composing the homotopy with the differential and the homotopy again recovers the homotopy.

@[simp]

theorem TauCeti.LinearSpecialContraction.homotopy_comp_dM_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 ∘ₗ dM ∘ₗ c.homotopy ∘ₗ f = c.homotopy ∘ₗ f

The homotopy-differential-homotopy identity with a further factor on the right.

@[simp]

theorem TauCeti.LinearSpecialContraction.homotopy_dM_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 (dM (c.homotopy x)) = c.homotopy x

The homotopy-differential-homotopy identity evaluated on an element.

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.

@[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.