Contractions of ℕ-indexed cochain complexes onto degree 0

Let K be a cochain complex indexed by ℕ in a preadditive category, and let h n : Kⁿ⁺¹ ⟶ Kⁿ be maps lowering the degree with $$d \circ h + h \circ d = 1 \text{ on } K^{n + 1}, \qquad h \circ d = 1 - P \text{ on } K^0$$ for an endomorphism P of K⁰. Then the composite of P with the differential vanishes (CochainComplex.comp_d_zero_eq_zero_of_d_comp_eq), so P placed in degree 0 is an endomorphism of K (CochainComplex.ofDegreeZero), and the maps h form a homotopy from the identity of K to it (CochainComplex.homotopyOfDCompEq). For a complex of modules, every positive-degree cocycle φ is the coboundary of h φ (CochainComplex.d_hom_apply_of_d_comp_eq).

This is the formal part shared by the contractions of cochain complexes that insert an argument weighted by an averaging or cutoff function: the contraction of the cochains of a groupoid nerve TauCeti.nerveCochainComplex.cutoffHomotopy, and those of inhomogeneous group cochains TauCeti.groupCohomology.homotopyOfDCompEq.

Main declarations

• CochainComplex.ofDegreeZero: an endomorphism of K⁰ whose composite with the differential vanishes, placed in degree 0, as an endomorphism of K.
• CochainComplex.homotopyOfDCompEq: the homotopy from the identity to CochainComplex.ofDegreeZero.
• CochainComplex.d_hom_apply_of_d_comp_eq: the explicit primitive of a positive-degree cocycle.

def CochainComplex.ofDegreeZero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (K : CochainComplex V ℕ) (P : K.X 0 ⟶ K.X 0) (hP : CategoryTheory.CategoryStruct.comp P (K.d 0 1) = 0) : K ⟶ K

An endomorphism P of K⁰ with P ≫ d = 0, placed in degree 0, as an endomorphism of the cochain complex K: it is P in degree 0 and zero in positive degrees.

@[simp]

theorem CochainComplex.ofDegreeZero_f_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {K : CochainComplex V ℕ} {P : K.X 0 ⟶ K.X 0} (hP : CategoryTheory.CategoryStruct.comp P (K.d 0 1) = 0) : (K.ofDegreeZero P hP).f 0 = P

In degree 0, CochainComplex.ofDegreeZero K P hP is P.

@[simp]

theorem CochainComplex.ofDegreeZero_f_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {K : CochainComplex V ℕ} {P : K.X 0 ⟶ K.X 0} (hP : CategoryTheory.CategoryStruct.comp P (K.d 0 1) = 0) (n : ℕ) : (K.ofDegreeZero P hP).f (n + 1) = 0

In positive degrees, CochainComplex.ofDegreeZero K P hP is zero.

theorem CochainComplex.comp_d_zero_eq_zero_of_d_comp_eq {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {K : CochainComplex V ℕ} {P : K.X 0 ⟶ K.X 0} {h : (n : ℕ) → K.X (n + 1) ⟶ K.X n} (hd : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (K.d (n + 1) (n + 2)) (h (n + 1)) + CategoryTheory.CategoryStruct.comp (h n) (K.d n (n + 1)) = CategoryTheory.CategoryStruct.id (K.X (n + 1))) (hd₀ : CategoryTheory.CategoryStruct.comp (K.d 0 1) (h 0) = CategoryTheory.CategoryStruct.id (K.X 0) - P) : CategoryTheory.CategoryStruct.comp P (K.d 0 1) = 0

If d ∘ h + h ∘ d = 1 in positive degrees and h ∘ d = 1 - P in degree 0, then the composite of P with the differential vanishes.

noncomputable def CochainComplex.homotopyOfDCompEq {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {K : CochainComplex V ℕ} {P : K.X 0 ⟶ K.X 0} {h : (n : ℕ) → K.X (n + 1) ⟶ K.X n} (hd : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (K.d (n + 1) (n + 2)) (h (n + 1)) + CategoryTheory.CategoryStruct.comp (h n) (K.d n (n + 1)) = CategoryTheory.CategoryStruct.id (K.X (n + 1))) (hd₀ : CategoryTheory.CategoryStruct.comp (K.d 0 1) (h 0) = CategoryTheory.CategoryStruct.id (K.X 0) - P) : Homotopy (CategoryTheory.CategoryStruct.id K) (K.ofDegreeZero P ⋯)

The contraction defined by maps lowering the degree. If d ∘ h + h ∘ d = 1 in positive degrees and h ∘ d = 1 - P in degree 0, then the identity of K is homotopic to P placed in degree 0, through the homotopy whose component from degree n + 1 to degree n is h n (CochainComplex.homotopyOfDCompEq_hom_succ).

@[simp]

theorem CochainComplex.homotopyOfDCompEq_hom_succ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {K : CochainComplex V ℕ} {P : K.X 0 ⟶ K.X 0} {h : (n : ℕ) → K.X (n + 1) ⟶ K.X n} (hd : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (K.d (n + 1) (n + 2)) (h (n + 1)) + CategoryTheory.CategoryStruct.comp (h n) (K.d n (n + 1)) = CategoryTheory.CategoryStruct.id (K.X (n + 1))) (hd₀ : CategoryTheory.CategoryStruct.comp (K.d 0 1) (h 0) = CategoryTheory.CategoryStruct.id (K.X 0) - P) (n : ℕ) : (homotopyOfDCompEq hd hd₀).hom (n + 1) n = h n

The component of CochainComplex.homotopyOfDCompEq from degree n + 1 to degree n is h n.

theorem CochainComplex.d_hom_apply_of_d_comp_eq {R : Type u_1} [Ring R] {K : CochainComplex (ModuleCat R) ℕ} {h : (n : ℕ) → K.X (n + 1) ⟶ K.X n} {n : ℕ} (hd : CategoryTheory.CategoryStruct.comp (K.d (n + 1) (n + 2)) (h (n + 1)) + CategoryTheory.CategoryStruct.comp (h n) (K.d n (n + 1)) = CategoryTheory.CategoryStruct.id (K.X (n + 1))) {φ : ↑(K.X (n + 1))} (hφ : (ModuleCat.Hom.hom (K.d (n + 1) (n + 2))) φ = 0) : (ModuleCat.Hom.hom (K.d n (n + 1))) ((ModuleCat.Hom.hom (h n)) φ) = φ

The explicit primitive of a positive-degree cocycle. For a cochain complex of modules, if d ∘ h + h ∘ d = 1 on Kⁿ⁺¹, then a cocycle φ of degree n + 1 is the coboundary of h φ.