The differential onto the boundaries

Let K be a homological complex. Write Zⱼ for its cycles in degree j, Hⱼ for its homology and Bⱼ = ker (Zⱼ ⟶ Hⱼ) for its boundaries, the kernel of the projection of the cycles onto the homology. The differential Kᵢ ⟶ Kⱼ corestricts to a morphism K.toBoundaries i j : Kᵢ ⟶ Bⱼ; this needs only zero morphisms and the existence of Hⱼ and Bⱼ. In an abelian category, for a relation i → j of the shape it is the cokernel of the inclusion Zᵢ ⟶ Kᵢ of the cycles (HomologicalComplex.toBoundariesIsCokernel), so that 0 ⟶ Zᵢ ⟶ Kᵢ ⟶ Bⱼ ⟶ 0 is short exact.

Together with 0 ⟶ Bⱼ ⟶ Zⱼ ⟶ Hⱼ ⟶ 0, this is the decomposition of a complex into cycles, boundaries and homology, used for splitting complexes and for the universal coefficient sequence.

Main declarations

• HomologicalComplex.toBoundaries: the corestriction Kᵢ ⟶ Bⱼ of the differential.
• HomologicalComplex.epi_toBoundaries: it is an epimorphism for a relation i → j.
• HomologicalComplex.toBoundariesIsCokernel: it is then the cokernel of Zᵢ ⟶ Kᵢ.
• HomologicalComplex.ExactAt.isIso_kernel_ι_homologyπ: at a degree where K is exact, the boundaries are all of the cycles.

noncomputable def HomologicalComplex.toBoundaries {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : ι) [K.HasHomology j] [CategoryTheory.Limits.HasKernel (K.homologyπ j)] : K.X i ⟶ CategoryTheory.Limits.kernel (K.homologyπ j)

The corestriction Kᵢ ⟶ Bⱼ of the differential to the boundaries Bⱼ = ker (Zⱼ ⟶ Hⱼ).

@[simp]

theorem HomologicalComplex.toBoundaries_ι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : ι) [K.HasHomology j] [CategoryTheory.Limits.HasKernel (K.homologyπ j)] : CategoryTheory.CategoryStruct.comp (K.toBoundaries i j) (CategoryTheory.Limits.kernel.ι (K.homologyπ j)) = K.toCycles i j

The corestriction of the differential to the boundaries, followed by the inclusion of the boundaries into the cycles, is the corestriction of the differential to the cycles.

@[simp]

theorem HomologicalComplex.toBoundaries_ι_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : ι) [K.HasHomology j] [CategoryTheory.Limits.HasKernel (K.homologyπ j)] {Z : C} (h : K.cycles j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.toBoundaries i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (K.homologyπ j)) h) = CategoryTheory.CategoryStruct.comp (K.toCycles i j) h

The corestriction of the differential to the boundaries, followed by the inclusion of the boundaries into the cycles, is the corestriction of the differential to the cycles.

@[simp]

theorem HomologicalComplex.iCycles_toBoundaries {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] [CategoryTheory.Limits.HasKernel (K.homologyπ j)] : CategoryTheory.CategoryStruct.comp (K.iCycles i) (K.toBoundaries i j) = 0

The corestriction of the differential to the boundaries vanishes on the cycles.

@[simp]

theorem HomologicalComplex.iCycles_toBoundaries_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (i j : ι) [K.HasHomology i] [K.HasHomology j] [CategoryTheory.Limits.HasKernel (K.homologyπ j)] {Z : C} (h : CategoryTheory.Limits.kernel (K.homologyπ j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (K.toBoundaries i j) h) = CategoryTheory.CategoryStruct.comp 0 h

The corestriction of the differential to the boundaries vanishes on the cycles.

@[simp]

theorem HomologicalComplex.d_toBoundaries {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (h i j : ι) [K.HasHomology j] [CategoryTheory.Limits.HasKernel (K.homologyπ j)] : CategoryTheory.CategoryStruct.comp (K.d h i) (K.toBoundaries i j) = 0

The corestriction of the differential to the boundaries vanishes on boundaries.

@[simp]

theorem HomologicalComplex.d_toBoundaries_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (h i j : ι) [K.HasHomology j] [CategoryTheory.Limits.HasKernel (K.homologyπ j)] {Z : C} (h✝ : CategoryTheory.Limits.kernel (K.homologyπ j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.d h i) (CategoryTheory.CategoryStruct.comp (K.toBoundaries i j) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The corestriction of the differential to the boundaries vanishes on boundaries.

theorem HomologicalComplex.ExactAt.isIso_kernel_ι_homologyπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] {K : HomologicalComplex C c} {j : ι} [K.HasHomology j] [CategoryTheory.Limits.HasKernel (K.homologyπ j)] (hj : K.ExactAt j) : CategoryTheory.IsIso (CategoryTheory.Limits.kernel.ι (K.homologyπ j))

At a degree where a complex is exact, the boundaries Bⱼ = ker (Zⱼ ⟶ Hⱼ) are all of the cycles.

theorem HomologicalComplex.epi_toBoundaries {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Abelian C] (K : HomologicalComplex C c) {i j : ι} (hij : c.Rel i j) : CategoryTheory.Epi (K.toBoundaries i j)

For a relation i → j of the shape, the corestriction Kᵢ ⟶ Bⱼ of the differential is an epimorphism, because the homology Hⱼ is the cokernel of Kᵢ ⟶ Zⱼ.

noncomputable def HomologicalComplex.toBoundariesIsCokernel {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι} [CategoryTheory.Abelian C] (K : HomologicalComplex C c) {i j : ι} (hij : c.Rel i j) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (K.toBoundaries i j) ⋯)

For a relation i → j of the shape, the corestriction Kᵢ ⟶ Bⱼ of the differential is the cokernel of the inclusion Zᵢ ⟶ Kᵢ of the cycles: it is an epimorphism whose kernel is Zᵢ, the kernel of the differential.