# Documentation

Mathlib.CategoryTheory.Abelian.Homology

The object homology f g w, where w : f ≫ g = 0, can be identified with either a cokernel or a kernel. The isomorphism with a cokernel is homologyIsoCokernelLift, which was obtained elsewhere. In the case of an abelian category, this file shows the isomorphism with a kernel as well.

We use these isomorphisms to obtain the analogous api for homology:

• homology.ι is the map from homology f g w into the cokernel of f.
• homology.π' is the map from kernel g to homology f g w.
• homology.desc' constructs a morphism from homology f g w, when it is viewed as a cokernel.
• homology.lift constructs a morphism to homology f g w, when it is viewed as a kernel.
• Various small lemmas are proved as well, mimicking the API for (co)kernels. With these definitions and lemmas, the isomorphisms between homology and a (co)kernel need not be used directly.
@[inline, reducible]
abbrev CategoryTheory.Abelian.homologyC {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
A

The cokernel of kernel.lift g f w. This is isomorphic to homology f g w. See homologyIsoCokernelLift.

Instances For
@[inline, reducible]
abbrev CategoryTheory.Abelian.homologyK {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
A

The kernel of cokernel.desc f g w. This is isomorphic to homology f g w. See homologyIsoKernelDesc.

Instances For
@[inline, reducible]
abbrev CategoryTheory.Abelian.homologyCToK {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :

The canonical map from homologyC to homologyK. This is an isomorphism, and it is used in obtaining the API for homology f g w in the bottom of this file.

Instances For
instance CategoryTheory.Abelian.instMonoHomologyCHomologyKHomologyCToK {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
instance CategoryTheory.Abelian.instEpiHomologyCHomologyKHomologyCToK {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
instance CategoryTheory.Abelian.instIsIsoHomologyCHomologyKHomologyCToK {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
def homologyIsoKernelDesc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :

The homology associated to f and g is isomorphic to a kernel.

Instances For
def homology.π' {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :

The canonical map from the kernel of g to the homology of f and g.

Instances For
def homology.ι {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :

The canonical map from the homology of f and g to the cokernel of f.

Instances For
def homology.desc' {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {W : A} (e : ) (he : ) :
homology f g w W

Obtain a morphism from the homology, given a morphism from the kernel.

Instances For
def homology.lift {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {W : A} (e : ) (he : ) :
W homology f g w

Obtain a moprhism to the homology, given a morphism to the kernel.

Instances For
@[simp]
theorem homology.π'_desc'_assoc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {W : A} (e : ) (he : ) {Z : A} (h : W Z) :
@[simp]
theorem homology.π'_desc' {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {W : A} (e : ) (he : ) :
@[simp]
theorem homology.lift_ι_assoc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {W : A} (e : ) (he : ) {Z : A} (h : ) :
@[simp]
theorem homology.lift_ι {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {W : A} (e : ) (he : ) :
@[simp]
theorem homology.condition_π'_assoc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {Z : A} (h : homology f g w Z) :
@[simp]
theorem homology.condition_π' {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
@[simp]
theorem homology.condition_ι_assoc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {Z : A} (h : Z Z) :
@[simp]
theorem homology.condition_ι {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
theorem homology.hom_from_ext {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {W : A} (a : homology f g w W) (b : homology f g w W) (h : ) :
a = b
theorem homology.hom_to_ext {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {W : A} (a : W homology f g w) (b : W homology f g w) (h : ) :
a = b
@[simp]
theorem homology.π'_ι_assoc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {Z : A} (h : ) :
@[simp]
theorem homology.π'_ι {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
@[simp]
theorem homology.π'_eq_π_assoc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {Z : A} (h : homology f g w Z) :
@[simp]
theorem homology.π'_eq_π {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
= homology.π f g w
@[simp]
theorem homology.π'_map_assoc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {X' : A} {Y' : A} {Z' : A} (f' : X' Y') (g' : Y' Z') (w' : ) (α : ) (β : ) (h : α.right = β.left) {Z : A} (h : homology f' g' w' Z) :
@[simp]
theorem homology.π'_map {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {X' : A} {Y' : A} {Z' : A} (f' : X' Y') (g' : Y' Z') (w' : ) (α : ) (β : ) (h : α.right = β.left) :
theorem homology.map_eq_desc'_lift_left {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {X' : A} {Y' : A} {Z' : A} (f' : X' Y') (g' : Y' Z') (w' : ) (α : ) (β : ) (h : α.right = β.left) :
theorem homology.map_eq_lift_desc'_left {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {X' : A} {Y' : A} {Z' : A} (f' : X' Y') (g' : Y' Z') (w' : ) (α : ) (β : ) (h : α.right = β.left) :
theorem homology.map_eq_desc'_lift_right {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {X' : A} {Y' : A} {Z' : A} (f' : X' Y') (g' : Y' Z') (w' : ) (α : ) (β : ) (h : α.right = β.left) :
theorem homology.map_eq_lift_desc'_right {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {X' : A} {Y' : A} {Z' : A} (f' : X' Y') (g' : Y' Z') (w' : ) (α : ) (β : ) (h : α.right = β.left) :
@[simp]
theorem homology.map_ι_assoc {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {X' : A} {Y' : A} {Z' : A} (f' : X' Y') (g' : Y' Z') (w' : ) (α : ) (β : ) (h : α.right = β.left) {Z : A} (h : ) :
@[simp]
theorem homology.map_ι {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) {X' : A} {Y' : A} {Z' : A} (f' : X' Y') (g' : Y' Z') (w' : ) (α : ) (β : ) (h : α.right = β.left) :
noncomputable def CategoryTheory.Functor.homologyIso {A : Type u} {ι : Type u_1} {c : } {B : Type u_2} [] (F : ) (C : ) (j : ι) :
F.obj ()

When F is an exact additive functor, F(Hᵢ(X)) ≅ Hᵢ(F(X)) for X a complex.

Instances For
noncomputable def CategoryTheory.Functor.homologyFunctorIso {A : Type u} {ι : Type u_1} {c : } {B : Type u_2} [] (F : ) (i : ι) :

If F is an exact additive functor, then F commutes with Hᵢ (up to natural isomorphism).

Instances For