Abelian categories have homology

In this file, it is shown that all short complexes S in abelian categories have terms of type S.HomologyData.

The strategy of the proof is to study the morphism kernel.ι S.g ≫ cokernel.π S.f. We show that there is a LeftHomologyData for S for which the H field consists of the coimage of kernel.ι S.g ≫ cokernel.π S.f, while there is a RightHomologyData for which the H is the image of kernel.ι S.g ≫ cokernel.π S.f. The fact that these left and right homology data are compatible (i.e. provide a HomologyData) is obtained by using the coimage-image isomorphism in abelian categories.

noncomputable def CategoryTheory.ShortComplex.abelianImageToKernel {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Abelian.image S.f ⟶ Limits.kernel S.g

The canonical morphism Abelian.image S.f ⟶ kernel S.g for a short complex S in an abelian category.

@[simp]

theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp S.abelianImageToKernel (Limits.kernel.ι S.g) = Abelian.image.ι S.f

@[simp]

theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {Z : C} (h : S.X₂ ⟶ Z) : CategoryStruct.comp S.abelianImageToKernel (CategoryStruct.comp (Limits.kernel.ι S.g) h) = CategoryStruct.comp (Abelian.image.ι S.f) h

instance CategoryTheory.ShortComplex.instMonoAbelianImageToKernel {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Mono S.abelianImageToKernel

theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp S.abelianImageToKernel (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f)) = 0

theorem CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {Z : C} (h : Limits.cokernel S.f ⟶ Z) : CategoryStruct.comp S.abelianImageToKernel (CategoryStruct.comp (Limits.kernel.ι S.g) (CategoryStruct.comp (Limits.cokernel.π S.f) h)) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.ShortComplex.abelianImageToKernelIsKernel {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Limits.IsLimit (Limits.KernelFork.ofι S.abelianImageToKernel ⋯)

Abelian.image S.f is the kernel of kernel.ι S.g ≫ cokernel.π S.f

noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : S.LeftHomologyData

The canonical LeftHomologyData of a short complex S in an abelian category, for which the H field is Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f).

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).π = Limits.cokernel.π (Limits.kernel.ι (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f)))

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).K = Limits.kernel S.g

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).i = Limits.kernel.ι S.g

@[simp]

theorem CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).H = Abelian.coimage (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f))

noncomputable def CategoryTheory.ShortComplex.cokernelToAbelianCoimage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Limits.cokernel S.f ⟶ Abelian.coimage S.g

The canonical morphism cokernel S.f ⟶ Abelian.coimage S.g for a short complex S in an abelian category.

@[simp]

theorem CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp (Limits.cokernel.π S.f) S.cokernelToAbelianCoimage = Abelian.coimage.π S.g

@[simp]

theorem CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) {Z : C} (h : Abelian.coimage S.g ⟶ Z) : CategoryStruct.comp (Limits.cokernel.π S.f) (CategoryStruct.comp S.cokernelToAbelianCoimage h) = CategoryStruct.comp (Abelian.coimage.π S.g) h

instance CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Epi S.cokernelToAbelianCoimage

theorem CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : CategoryStruct.comp (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f)) S.cokernelToAbelianCoimage = 0

noncomputable def CategoryTheory.ShortComplex.cokernelToAbelianCoimageIsCokernel {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : Limits.IsColimit (Limits.CokernelCofork.ofπ S.cokernelToAbelianCoimage ⋯)

Abelian.coimage S.g is the cokernel of kernel.ι S.g ≫ cokernel.π S.f

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.ofAbelian {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : S.RightHomologyData

The canonical RightHomologyData of a short complex S in an abelian category, for which the H field is Abelian.image (kernel.ι S.g ≫ cokernel.π S.f).

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).p = Limits.cokernel.π S.f

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).ι = Limits.kernel.ι (Limits.cokernel.π (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f)))

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_Q {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).Q = Limits.cokernel S.f

@[simp]

theorem CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : (ofAbelian S).H = Abelian.image (CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f))

noncomputable def CategoryTheory.ShortComplex.HomologyData.ofAbelian {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) : S.HomologyData

The canonical HomologyData of a short complex S in an abelian category.

instance CategoryTheory.categoryWithHomology_of_abelian {C : Type u} [Category.{v, u} C] [Abelian C] : CategoryWithHomology C