Opcycles as retracts of terms

Let K be a cochain complex indexed by ℤ, and i + 1 = j. If the projection K^i ⟶ K.opcycles i factors as the differential K^i ⟶ K^j followed by some r : K^j ⟶ K.opcycles i, then K.opcycles j, the cokernel of the differential into K^j, is a retract of K^j. Such an r comes from a null-homotopy of the projection of K onto its opcycles in degree i, seen as a chain map to the complex concentrated in degree i. In particular, K.opcycles j is then projective when K^j is.

Main definitions

• CochainComplex.retractOpcycles: K.opcycles j is a retract of K^j, given such an r.
• CochainComplex.toSingleOpcycles: the projection of K onto its opcycles in degree i, as a chain map to the complex concentrated in degree i.
• CochainComplex.retractOpcyclesOfHomotopy: K.opcycles (i + 1) is a retract of K^(i + 1) when K.toSingleOpcycles i is null-homotopic.

noncomputable def CochainComplex.retractOpcycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) {i j : ℤ} (hij : i + 1 = j) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] (r : K.X j ⟶ HomologicalComplex.opcycles K i) (hr : CategoryTheory.CategoryStruct.comp (K.d i j) r = HomologicalComplex.pOpcycles K i) : CategoryTheory.Retract (HomologicalComplex.opcycles K j) (K.X j)

If the differential K^i ⟶ K^j followed by r : K^j ⟶ K.opcycles i is the projection K^i ⟶ K.opcycles i, then K.opcycles j is a retract of K^j.

noncomputable def CochainComplex.toSingleOpcycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] (i : ℤ) [HomologicalComplex.HasHomology K i] : K ⟶ (HomologicalComplex.single C (ComplexShape.up ℤ) i).obj (HomologicalComplex.opcycles K i)

The projection of K onto its opcycles in degree i, as a chain map to the complex concentrated in degree i.

@[simp]

theorem CochainComplex.toSingleOpcycles_f_self {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] (i : ℤ) [HomologicalComplex.HasHomology K i] : (K.toSingleOpcycles i).f i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles K i) (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) i (HomologicalComplex.opcycles K i)).inv

The component of K.toSingleOpcycles i in degree i is the projection onto the opcycles.

noncomputable def CochainComplex.retractOpcyclesOfHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) [CategoryTheory.Limits.HasZeroObject C] {i j : ℤ} (hij : i + 1 = j) [HomologicalComplex.HasHomology K i] [HomologicalComplex.HasHomology K j] (h : Homotopy (K.toSingleOpcycles i) 0) : CategoryTheory.Retract (HomologicalComplex.opcycles K j) (K.X j)

If the projection of K onto its opcycles in degree i is null-homotopic as a chain map to the complex concentrated in degree i, then K.opcycles j is a retract of K^j, where j = i + 1.