Documentation

Mathlib.Algebra.Homology.ShortComplex.Abelian

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.

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

Equations

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.

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.

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

Equations

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.

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.

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.