Zero-differential homology models

This file packages the homology objects of a cochain complex in an abelian category as a new complex with zero differential. It makes no formality claim: an equivalence with the original complex requires additional splitting hypotheses and belongs in a specialization.

noncomputable def CochainComplex.homologyModel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) : CochainComplex A ℤ

The zero-differential complex whose object in degree i is the homology of K in degree i.

Equations

• K.homologyModel = CochainComplex.of (fun (i : ℤ) => HomologicalComplex.homology K i) (fun (x : ℤ) => 0) ⋯

@[simp]

theorem CochainComplex.homologyModel_X {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) (i : ℤ) : K.homologyModel.X i = HomologicalComplex.homology K i

@[simp]

theorem CochainComplex.homologyModel_d {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) (i j : ℤ) : K.homologyModel.d i j = 0