# Documentation

Mathlib.CategoryTheory.Abelian.Exact

# Exact sequences in abelian categories #

In an abelian category, we get several interesting results related to exactness which are not true in more general settings.

## Main results #

• (f, g) is exact if and only if f ≫ g = 0 and kernel.ι g ≫ cokernel.π f = 0. This characterisation tends to be less cumbersome to work with than the original definition involving the comparison map image f ⟶ kernel g.
• If (f, g) is exact, then image.ι f has the universal property of the kernel of g.
• f is a monomorphism iff kernel.ι f = 0 iff Exact 0 f, and f is an epimorphism iff cokernel.π = 0 iff Exact f 0.
• A faithful functor between abelian categories that preserves zero morphisms reflects exact sequences.
• X ⟶ Y ⟶ Z ⟶ 0 is exact if and only if the second map is a cokernel of the first, and 0 ⟶ X ⟶ Y ⟶ Z is exact if and only if the first map is a kernel of the second.
• An exact functor preserves exactness, more specifically, F preserves finite colimits and finite limits, if and only if Exact f g implies Exact (F.map f) (F.map g).
theorem CategoryTheory.Abelian.exact_iff_image_eq_kernel {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

In an abelian category, a pair of morphisms f : X ⟶ Y, g : Y ⟶ Z is exact iff imageSubobject f = kernelSubobject g.

theorem CategoryTheory.Abelian.exact_iff {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
theorem CategoryTheory.Abelian.exact_iff' {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) {cg : } (hg : ) (hf : ) :
theorem CategoryTheory.Abelian.exact_tfae {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
theorem CategoryTheory.Abelian.IsEquivalence.exact_iff {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) {D : Type u₁} [] (F : ) :
CategoryTheory.Exact (F.map f) (F.map g)
theorem CategoryTheory.Abelian.exact_epi_comp_iff {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) {W : C} (h : W X) :

The dual result is true even in non-abelian categories, see CategoryTheory.exact_comp_mono_iff.

def CategoryTheory.Abelian.isLimitImage {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : ) :

If (f, g) is exact, then Abelian.image.ι f is a kernel of g.

Instances For
def CategoryTheory.Abelian.isLimitImage' {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : ) :

If (f, g) is exact, then image.ι f is a kernel of g.

Instances For
def CategoryTheory.Abelian.isColimitCoimage {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : ) :

If (f, g) is exact, then Abelian.coimage.π g is a cokernel of f.

Instances For
def CategoryTheory.Abelian.isColimitImage {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : ) :

If (f, g) is exact, then factorThruImage g is a cokernel of f.

Instances For
theorem CategoryTheory.Abelian.exact_cokernel {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Abelian.mono_cokernel_desc_of_exact {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : ) :
theorem CategoryTheory.Abelian.isIso_cokernel_desc_of_exact_of_epi {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (ex : ) :

If ex : Exact f g and epi g, then cokernel.desc _ _ ex.w is an isomorphism.

theorem CategoryTheory.Abelian.cokernel.desc.inv_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (ex : ) {Z : C} (h : ) :
theorem CategoryTheory.Abelian.cokernel.desc.inv {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (ex : ) :
let_fun this := (_ : );
theorem CategoryTheory.Abelian.isIso_kernel_lift_of_exact_of_mono {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (ex : ) :
theorem CategoryTheory.Abelian.kernel.lift.inv_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (ex : ) {Z : C} (h : Y Z) :
theorem CategoryTheory.Abelian.kernel.lift.inv {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (ex : ) :
let_fun this := (_ : );
def CategoryTheory.Abelian.isColimitOfExactOfEpi {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : ) :

If X ⟶ Y ⟶ Z ⟶ 0 is exact, then the second map is a cokernel of the first.

Instances For
def CategoryTheory.Abelian.isLimitOfExactOfMono {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : ) :

If 0 ⟶ X ⟶ Y ⟶ Z is exact, then the first map is a kernel of the second.

Instances For
theorem CategoryTheory.Abelian.exact_of_is_cokernel {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (w : ) :
theorem CategoryTheory.Abelian.exact_of_is_kernel {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (w : ) :
theorem CategoryTheory.Abelian.exact_iff_exact_image_ι {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
theorem CategoryTheory.Abelian.exact_iff_exact_coimage_π {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
theorem CategoryTheory.Abelian.tfae_mono {C : Type u₁} [] {X : C} {Y : C} (Z : C) (f : X Y) :
theorem CategoryTheory.Abelian.mono_iff_kernel_ι_eq_zero {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Abelian.tfae_epi {C : Type u₁} [] {X : C} {Y : C} (Z : C) (f : X Y) :
theorem CategoryTheory.Abelian.epi_iff_cokernel_π_eq_zero {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Abelian.Exact.op {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (h : ) :
theorem CategoryTheory.Abelian.Exact.op_iff {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :
theorem CategoryTheory.Abelian.Exact.unop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (g : X Y) (f : Y Z) (h : ) :
CategoryTheory.Exact f.unop g.unop
theorem CategoryTheory.Abelian.Exact.unop_iff {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (g : X Y) (f : Y Z) :
CategoryTheory.Exact f.unop g.unop
theorem CategoryTheory.Functor.map_exact {A : Type u₁} {B : Type u₂} [] [] (L : ) {X : A} {Y : A} {Z : A} (f : X Y) (g : Y Z) (e1 : ) :
CategoryTheory.Exact (L.map f) (L.map g)

A functor preserving finite limits and finite colimits preserves exactness. The converse result is also true, see Functor.preservesFiniteLimitsOfMapExact and Functor.preservesFiniteColimitsOfMapExact.

theorem CategoryTheory.Functor.preservesZeroMorphisms_of_map_exact {A : Type u₁} {B : Type u₂} [] [] (L : ) (h : ∀ ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, CategoryTheory.Exact (L.map f) (L.map g)) :

A functor which preserves exactness preserves zero morphisms.

theorem CategoryTheory.Functor.preservesMonomorphisms_of_map_exact {A : Type u₁} {B : Type u₂} [] [] (L : ) (h : ∀ ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, CategoryTheory.Exact (L.map f) (L.map g)) :

A functor which preserves exactness preserves monomorphisms.

theorem CategoryTheory.Functor.preservesEpimorphisms_of_map_exact {A : Type u₁} {B : Type u₂} [] [] (L : ) (h : ∀ ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, CategoryTheory.Exact (L.map f) (L.map g)) :

A functor which preserves exactness preserves epimorphisms.

def CategoryTheory.Functor.preservesKernelsOfMapExact {A : Type u₁} {B : Type u₂} [] [] (L : ) (h : ∀ ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, CategoryTheory.Exact (L.map f) (L.map g)) (X : A) (Y : A) (f : X Y) :

A functor which preserves exactness preserves kernels.

Instances For
def CategoryTheory.Functor.preservesCokernelsOfMapExact {A : Type u₁} {B : Type u₂} [] [] (L : ) (h : ∀ ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, CategoryTheory.Exact (L.map f) (L.map g)) (X : A) (Y : A) (f : X Y) :

A functor which preserves exactness preserves zero cokernels.

Instances For
def CategoryTheory.Functor.preservesFiniteLimitsOfMapExact {A : Type u₁} {B : Type u₂} [] [] (L : ) (h : ∀ ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, CategoryTheory.Exact (L.map f) (L.map g)) :

A functor which preserves exactness is left exact, i.e. preserves finite limits. This is part of the inverse implication to Functor.map_exact.

Instances For
def CategoryTheory.Functor.preservesFiniteColimitsOfMapExact {A : Type u₁} {B : Type u₂} [] [] (L : ) (h : ∀ ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, CategoryTheory.Exact (L.map f) (L.map g)) :

A functor which preserves exactness is right exact, i.e. preserves finite colimits. This is part of the inverse implication to Functor.map_exact.

Instances For

A functor preserving zero morphisms, monos, and cokernels preserves finite limits.

Instances For

A functor preserving zero morphisms, epis, and kernels preserves finite colimits.

Instances For