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

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

@[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 (CategoryTheory.ShortComplex.abelianImageToKernel S) (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 (CategoryTheory.ShortComplex.abelianImageToKernel S) (CategoryTheory.Limits.kernel.ι S.g) = CategoryTheory.Abelian.image.ι S.f

instance CategoryTheory.ShortComplex.instMonoImagePreadditiveHasZeroMorphismsToPreadditiveHasKernels_of_hasEqualizersHasEqualizersHasCokernels_of_hasCoequalizersHasCoequalizersX₁X₂FKernelX₃GHas_limitAbelianImageToKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Mono (CategoryTheory.ShortComplex.abelianImageToKernel S)

Equations

• (_ : CategoryTheory.Mono (CategoryTheory.ShortComplex.abelianImageToKernel S)) = (_ : CategoryTheory.Mono (CategoryTheory.ShortComplex.abelianImageToKernel S))

@[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 (CategoryTheory.ShortComplex.abelianImageToKernel S) (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 (CategoryTheory.ShortComplex.abelianImageToKernel S) (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ι (CategoryTheory.ShortComplex.abelianImageToKernel S) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.abelianImageToKernel S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) = 0))

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_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_π {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_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) : CategoryTheory.ShortComplex.LeftHomologyData S

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

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

@[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 (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) 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) (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) = CategoryTheory.Abelian.coimage.π S.g

instance CategoryTheory.ShortComplex.instEpiCokernelPreadditiveHasZeroMorphismsToPreadditiveX₁X₂FHas_colimitHasCokernels_of_hasCoequalizersHasCoequalizersCoimageHasKernels_of_hasEqualizersHasEqualizersX₃GCokernelToAbelianCoimage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.Epi (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S)

Equations

• (_ : CategoryTheory.Epi (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S)) = (_ : CategoryTheory.Epi (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S))

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)) (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) = 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π (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) (CategoryTheory.ShortComplex.cokernelToAbelianCoimage S) = 0))

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_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

@[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

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

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) : CategoryTheory.ShortComplex.HomologyData S

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

• (_ : CategoryTheory.CategoryWithHomology C) = (_ : CategoryTheory.CategoryWithHomology C)

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 (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0) ≅ CategoryTheory.ShortComplex.homology S

Comparison isomorphism between two definitions of homology.

Equations

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