Contractions of cochain complexes and their normalization

A contraction of a cochain complex K onto a cochain complex L consists of an inclusion i : L ⟶ K, a projection p : K ⟶ L with p i = 1, and a degree -1 cochain h on K with

1 - i p = d h + h d.

Homological perturbation theory, and in particular the tree formula for transferred A∞ operations, needs a contraction which additionally satisfies the three side conditions

h i = 0, p h = 0, h h = 0.

Such data is a special contraction, classically a strong deformation retract. Demanding the side conditions of every caller would be a bad interface: they are not what a contraction is naturally produced with. This file therefore takes the weaker datum as the input and proves that it can always be normalized. TauCeti.Contraction.normalize turns an arbitrary contraction into a special one with the same i and p, changing only the homotopy.

The normalization is the classical two-step argument. Write Ψ = 1 - i p for the complementary idempotent. The first step replaces h by h₁ = Ψ h Ψ: this kills h i and p h because Ψ i = 0 and p Ψ = 0, and it is still a contracting homotopy because Ψ is idempotent and is a chain map. The second step replaces h₁ by h₂ = h₁ d h₁. The two annihilation conditions survive, and the new homotopy squares to zero: the degree -2 cochain h₁ h₁ is a cocycle, hence commutes with d, so h₂ h₂ contains the factor d (h₁ h₁) d = d d (h₁ h₁) = 0. That h₂ is still a contracting homotopy is visible from the equivalent form h₂ = h₁ - d (h₁ h₁), whose correction term is δ-closed. The two intermediate homotopies are private: a consumer needs TauCeti.Contraction.normalize and the side conditions it carries as a TauCeti.SpecialContraction, not the stages producing it.

Cochains and their differential are Mathlib's CochainComplex.HomComplex API. In degree -1 that differential is δ (-1) 0 h = h d + d h, with no sign, so it is exactly the operator the contracting equation constrains.

Main definitions

• TauCeti.Contraction: the weak input, a contraction of K onto L.
• TauCeti.Contraction.idem and TauCeti.Contraction.idemCompl: the idempotent i p cut out by a contraction, and its complement 1 - i p.
• TauCeti.SpecialContraction: a contraction satisfying the three side conditions.
• TauCeti.Contraction.normalize: the special contraction produced from a contraction. Its three side conditions are the TauCeti.SpecialContraction fields it carries.
• TauCeti.Contraction.homotopyEquiv: the homotopy equivalence between L and K underlying a contraction.

Main results

• TauCeti.Contraction.normalize_incl and TauCeti.Contraction.normalize_proj: normalization changes only the homotopy.
• TauCeti.SpecialContraction.normalize_toContraction: normalization is a retraction, so it leaves an already special contraction unchanged.
• TauCeti.Contraction.quasiIso_incl and TauCeti.Contraction.quasiIso_proj: both structure maps of a contraction are quasi-isomorphisms.

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.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.3.

structure TauCeti.Contraction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) : Type v

A contraction of a cochain complex K onto a cochain complex L: an inclusion incl, a projection proj retracting it, and a degree -1 cochain contracting the identity of K onto the resulting idempotent. No side conditions are imposed; TauCeti.Contraction.normalize supplies them.

• incl : L ⟶ K

  the inclusion of the retract

• proj : K ⟶ L

  the projection onto the retract

• homotopy : CochainComplex.HomComplex.Cochain K K (-1)

  the contracting homotopy, a cochain of degree -1

• incl_comp_proj : CategoryTheory.CategoryStruct.comp self.incl self.proj = CategoryTheory.CategoryStruct.id L

  the projection retracts the inclusion

• δ_homotopy : CochainComplex.HomComplex.δ (-1) 0 self.homotopy = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id K - CategoryTheory.CategoryStruct.comp self.proj self.incl)

  h d + d h is the complementary idempotent 1 - i p

theorem TauCeti.Contraction.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {K L : CochainComplex C ℤ} {x y : Contraction K L} (incl : x.incl = y.incl) (proj : x.proj = y.proj) (homotopy : x.homotopy = y.homotopy) : x = y

theorem TauCeti.Contraction.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {K L : CochainComplex C ℤ} {x y : Contraction K L} : x = y ↔ x.incl = y.incl ∧ x.proj = y.proj ∧ x.homotopy = y.homotopy

structure TauCeti.SpecialContraction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) extends TauCeti.Contraction K L : Type v

A special contraction, classically a strong deformation retract: a contraction whose homotopy satisfies the three side conditions h i = 0, p h = 0 and h h = 0.

• incl : L ⟶ K
• proj : K ⟶ L
• homotopy : CochainComplex.HomComplex.Cochain K K (-1)
• incl_comp_proj : CategoryTheory.CategoryStruct.comp self.incl self.proj = CategoryTheory.CategoryStruct.id L
• δ_homotopy : CochainComplex.HomComplex.δ (-1) 0 self.homotopy = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id K - CategoryTheory.CategoryStruct.comp self.proj self.incl)
• incl_comp_homotopy : (CochainComplex.HomComplex.Cochain.ofHom self.incl).comp self.homotopy _proof_3 = 0

  the homotopy annihilates the inclusion

• homotopy_comp_proj : self.homotopy.comp (CochainComplex.HomComplex.Cochain.ofHom self.proj) _proof_5 = 0

  the projection annihilates the homotopy

• homotopy_comp_homotopy : self.homotopy.comp self.homotopy _proof_7 = 0

  the homotopy squares to zero

theorem TauCeti.SpecialContraction.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {K L : CochainComplex C ℤ} {x y : SpecialContraction K L} : x = y ↔ x.incl = y.incl ∧ x.proj = y.proj ∧ x.homotopy = y.homotopy

theorem TauCeti.SpecialContraction.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {K L : CochainComplex C ℤ} {x y : SpecialContraction K L} (incl : x.incl = y.incl) (proj : x.proj = y.proj) (homotopy : x.homotopy = y.homotopy) : x = y

theorem TauCeti.Contraction.incl_comp_proj_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (self : Contraction K L) {Z : CochainComplex C ℤ} (h : L ⟶ Z) : CategoryTheory.CategoryStruct.comp self.incl (CategoryTheory.CategoryStruct.comp self.proj h) = h

the projection retracts the inclusion

def TauCeti.Contraction.idem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : K ⟶ K

The idempotent endomorphism i p of K cut out by a contraction.

Equations

• c.idem = CategoryTheory.CategoryStruct.comp c.proj c.incl

def TauCeti.Contraction.idemCompl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : K ⟶ K

The complementary idempotent 1 - i p of a contraction; it is the endomorphism which the contracting homotopy trivializes.

Equations

• c.idemCompl = CategoryTheory.CategoryStruct.id K - c.idem

theorem TauCeti.Contraction.idem_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : c.idem = CategoryTheory.CategoryStruct.comp c.proj c.incl

The defining equation of the idempotent cut out by a contraction.

theorem TauCeti.Contraction.idemCompl_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : c.idemCompl = CategoryTheory.CategoryStruct.id K - c.idem

The defining equation of the complementary idempotent of a contraction.

@[simp]

theorem TauCeti.Contraction.incl_comp_idem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : CategoryTheory.CategoryStruct.comp c.incl c.idem = c.incl

@[simp]

theorem TauCeti.Contraction.idem_comp_proj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : CategoryTheory.CategoryStruct.comp c.idem c.proj = c.proj

@[simp]

theorem TauCeti.Contraction.idem_comp_idem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : CategoryTheory.CategoryStruct.comp c.idem c.idem = c.idem

@[simp]

theorem TauCeti.Contraction.incl_comp_idemCompl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : CategoryTheory.CategoryStruct.comp c.incl c.idemCompl = 0

@[simp]

theorem TauCeti.Contraction.idemCompl_comp_proj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : CategoryTheory.CategoryStruct.comp c.idemCompl c.proj = 0

@[simp]

theorem TauCeti.Contraction.idemCompl_comp_idemCompl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : CategoryTheory.CategoryStruct.comp c.idemCompl c.idemCompl = c.idemCompl

def TauCeti.Contraction.normalize {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : SpecialContraction K L

Normalization of a contraction. Every contraction of cochain complexes can be replaced, without changing its inclusion or its projection, by one satisfying the three side conditions h i = 0, p h = 0 and h h = 0.

Equations

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

@[simp]

theorem TauCeti.Contraction.normalize_incl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : c.normalize.incl = c.incl

@[simp]

theorem TauCeti.Contraction.normalize_proj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : c.normalize.proj = c.proj

noncomputable def TauCeti.Contraction.homotopyIdemId {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : Homotopy c.idem (CategoryTheory.CategoryStruct.id K)

The homotopy from the idempotent i p to the identity of K given by a contraction.

Equations

• c.homotopyIdemId = (CochainComplex.HomComplex.Cochain.equivHomotopy c.idem (CategoryTheory.CategoryStruct.id K)).symm ⟨-c.homotopy, ⋯⟩

noncomputable def TauCeti.Contraction.homotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : HomotopyEquiv L K

A contraction exhibits L as homotopy equivalent to K.

Equations

• c.homotopyEquiv = { hom := c.incl, inv := c.proj, homotopyHomInvId := Homotopy.ofEq ⋯, homotopyInvHomId := c.homotopyIdemId }

@[simp]

theorem TauCeti.Contraction.homotopyEquiv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : c.homotopyEquiv.hom = c.incl

@[simp]

theorem TauCeti.Contraction.homotopyEquiv_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) : c.homotopyEquiv.inv = c.proj

theorem TauCeti.Contraction.quasiIso_incl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) [∀ (n : ℤ), HomologicalComplex.HasHomology K n] [∀ (n : ℤ), HomologicalComplex.HasHomology L n] : QuasiIso c.incl

The inclusion of a contraction is a quasi-isomorphism.

theorem TauCeti.Contraction.quasiIso_proj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (c : Contraction K L) [∀ (n : ℤ), HomologicalComplex.HasHomology K n] [∀ (n : ℤ), HomologicalComplex.HasHomology L n] : QuasiIso c.proj

The projection of a contraction is a quasi-isomorphism.

@[simp]

theorem TauCeti.SpecialContraction.idemCompl_comp_homotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (s : SpecialContraction K L) : (CochainComplex.HomComplex.Cochain.ofHom s.idemCompl).comp s.homotopy _proof_3 = s.homotopy

In a special contraction the complementary idempotent acts as the identity on the homotopy from the left, because h i = 0.

@[simp]

theorem TauCeti.SpecialContraction.homotopy_comp_idemCompl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (s : SpecialContraction K L) : s.homotopy.comp (CochainComplex.HomComplex.Cochain.ofHom s.idemCompl) _proof_5 = s.homotopy

In a special contraction the complementary idempotent acts as the identity on the homotopy from the right, because p h = 0.

@[simp]

theorem TauCeti.SpecialContraction.normalize_toContraction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} (s : SpecialContraction K L) : s.normalize = s

Normalization is a retraction: it leaves an already special contraction unchanged. In particular normalizing twice is the same as normalizing once.

def TauCeti.SpecialContraction.refl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : SpecialContraction K K

Every cochain complex is a special contraction of itself, with zero homotopy. This pins the orientation of the contracting equation: it has 1 - i p on the right, so the identity contraction has vanishing homotopy.

Equations

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

@[simp]

theorem TauCeti.SpecialContraction.refl_incl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : (refl K).incl = CategoryTheory.CategoryStruct.id K

@[simp]

theorem TauCeti.SpecialContraction.refl_proj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : (refl K).proj = CategoryTheory.CategoryStruct.id K

@[simp]

theorem TauCeti.SpecialContraction.refl_homotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) : (refl K).homotopy = 0