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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Abelian.image S.f ⟶ CategoryTheory.Limits.kernel S.g

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

Equations

• S.abelianImageToKernel = CategoryTheory.Limits.kernel.lift S.g (CategoryTheory.Abelian.image.ι S.f) ⋯

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.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).

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• S.cokernelToAbelianCoimage = CategoryTheory.Limits.cokernel.desc S.f (CategoryTheory.Abelian.coimage.π S.g) ⋯

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.ShortComplex.RightHomologyData.ofAbelian {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.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).

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.ShortComplex.homology'IsoHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : homology' S.f S.g ⋯ ≅ S.homology

Comparison isomorphism between two definitions of homology.

Equations

• S.homology'IsoHomology = homology'IsoCokernelLift S.f S.g ⋯ ≪≫ S.homologyIsoCokernelLift.symm