# 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 homology'IsoCokernelLift, 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.

Note: As part of the homology refactor, it is planned to remove the definitions in this file, because it can be replaced by the content of Algebra.Homology.ShortComplex.Homology.

@[reducible, inline]
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.

Equations
Instances For
@[reducible, inline]
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.

Equations
Instances For
@[reducible, inline]
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Abelian.instMonoHomologyCToK {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
Equations
• =
instance CategoryTheory.Abelian.instEpiHomologyCToK {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
Equations
• =
instance CategoryTheory.Abelian.instIsIsoHomologyCToK {A : Type u} {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (w : ) :
Equations
• =
def homology'IsoKernelDesc {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.

Equations
• = ().trans
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.

Equations
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.

Equations
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.

Equations
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 morphism to the homology, given a morphism to the kernel.

Equations
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 : ) :
@[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) :
homology'.map w w' α β h = homology'.desc' f g w (homology'.lift f' g' w' )
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) :
homology'.map w w' α β h = homology'.lift f' g' w' ()
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) :
homology'.map w w' α β h = homology'.desc' f g w (homology'.lift f' g' w' )
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) :
homology'.map w w' α β h = homology'.lift 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 : ) :
@[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.homology'Iso {A : Type u} {ι : Type u_1} {c : } {B : Type u_2} [] (F : ) [F.Additive] (C : ) (j : ι) :
F.obj (C.homology' j) ((F.mapHomologicalComplex c).obj C).homology' j

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Functor.homology'FunctorIso {A : Type u} {ι : Type u_1} {c : } {B : Type u_2} [] (F : ) [F.Additive] (i : ι) :
().comp F (F.mapHomologicalComplex c).comp ()

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

Equations
Instances For