# mathlib3documentation

category_theory.abelian.exact

# Exact sequences in abelian categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 category_theory.abelian.exact_iff_image_eq_kernel {C : Type u₁} {X Y 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 image_subobject f = kernel_subobject g.

theorem category_theory.abelian.exact_iff {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) :
theorem category_theory.abelian.exact_iff' {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (hg : category_theory.limits.is_limit cg)  :
f g = 0
theorem category_theory.abelian.exact_tfae {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) :
theorem category_theory.abelian.is_equivalence.exact_iff {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) {D : Type u₁} (F : C D)  :
theorem category_theory.abelian.exact_epi_comp_iff {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) {W : C} (h : W X)  :

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

noncomputable def category_theory.abelian.is_limit_image {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : g) :

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

Equations
• = (λ (W : C) (u : W Y) (hu : u g = 0), _ _
noncomputable def category_theory.abelian.is_limit_image' {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : g) :

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

Equations
noncomputable def category_theory.abelian.is_colimit_coimage {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : g) :

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

Equations
• = (λ (W : C) (u : Y W) (hu : f u = 0), _ _
noncomputable def category_theory.abelian.is_colimit_image {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : g) :

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

Equations
theorem category_theory.abelian.exact_cokernel {C : Type u₁} {X Y : C} (f : X Y) :
@[protected, instance]
def category_theory.abelian.category_theory.limits.cokernel.desc.category_theory.mono {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : g) :
@[protected, instance]
def category_theory.abelian.category_theory.limits.cokernel.desc.category_theory.is_iso {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (ex : g)  :

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

@[simp]
theorem category_theory.abelian.cokernel.desc.inv_assoc {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (ex : g) {X' : C} (f' : X') :
@[simp]
theorem category_theory.abelian.cokernel.desc.inv {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (ex : g) :
@[protected, instance]
def category_theory.abelian.category_theory.limits.kernel.lift.category_theory.is_iso {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (ex : g)  :
@[simp]
theorem category_theory.abelian.kernel.lift.inv_assoc {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (ex : g) {X' : C} (f' : Y X') :
f f' =
@[simp]
theorem category_theory.abelian.kernel.lift.inv {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (ex : g) :
noncomputable def category_theory.abelian.is_colimit_of_exact_of_epi {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : g) :

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

Equations
noncomputable def category_theory.abelian.is_limit_of_exact_of_mono {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : g) :

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

Equations
theorem category_theory.abelian.exact_of_is_cokernel {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (w : f g = 0)  :
theorem category_theory.abelian.exact_of_is_kernel {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (w : f g = 0)  :
theorem category_theory.abelian.exact_iff_exact_image_ι {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) :
theorem category_theory.abelian.exact_iff_exact_coimage_π {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) :
theorem category_theory.abelian.tfae_mono {C : Type u₁} {X Y : C} (Z : C) (f : X Y) :
theorem category_theory.abelian.mono_iff_kernel_ι_eq_zero {C : Type u₁} {X Y : C} (f : X Y) :
theorem category_theory.abelian.tfae_epi {C : Type u₁} {X Y : C} (Z : C) (f : X Y) :
theorem category_theory.abelian.epi_iff_cokernel_π_eq_zero {C : Type u₁} {X Y : C} (f : X Y) :
theorem category_theory.abelian.exact.op {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) (h : g) :
theorem category_theory.abelian.exact.op_iff {C : Type u₁} {X Y Z : C} (f : X Y) (g : Y Z) :
theorem category_theory.abelian.exact.unop {C : Type u₁} {X Y Z : Cᵒᵖ} (g : X Y) (f : Y Z) (h : f) :
theorem category_theory.abelian.exact.unop_iff {C : Type u₁} {X Y Z : Cᵒᵖ} (g : X Y) (f : Y Z) :
@[protected, instance]
Equations
theorem category_theory.functor.map_exact {A : Type u₁} {B : Type u₂} (L : A B) {X Y Z : A} (f : X Y) (g : Y Z) (e1 : g) :

A functor preserving finite limits and finite colimits preserves exactness. The converse result is also true, see functor.preserves_finite_limits_of_map_exact and functor.preserves_finite_colimits_of_map_exact.

theorem category_theory.functor.preserves_zero_morphisms_of_map_exact {A : Type u₁} {B : Type u₂} (L : A B) (h : ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, category_theory.exact (L.map f) (L.map g)) :

A functor which preserves exactness preserves zero morphisms.

theorem category_theory.functor.preserves_monomorphisms_of_map_exact {A : Type u₁} {B : Type u₂} (L : A B) (h : ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, category_theory.exact (L.map f) (L.map g)) :

A functor which preserves exactness preserves monomorphisms.

theorem category_theory.functor.preserves_epimorphisms_of_map_exact {A : Type u₁} {B : Type u₂} (L : A B) (h : ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, category_theory.exact (L.map f) (L.map g)) :

A functor which preserves exactness preserves epimorphisms.

noncomputable def category_theory.functor.preserves_kernels_of_map_exact {A : Type u₁} {B : Type u₂} (L : A B) (h : ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, category_theory.exact (L.map f) (L.map g)) (X Y : A) (f : X Y) :

A functor which preserves exactness preserves kernels.

Equations
noncomputable def category_theory.functor.preserves_cokernels_of_map_exact {A : Type u₁} {B : Type u₂} (L : A B) (h : ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, category_theory.exact (L.map f) (L.map g)) (X Y : A) (f : X Y) :

A functor which preserves exactness preserves zero cokernels.

Equations
noncomputable def category_theory.functor.preserves_finite_limits_of_map_exact {A : Type u₁} {B : Type u₂} (L : A B) (h : ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, category_theory.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.

Equations
noncomputable def category_theory.functor.preserves_finite_colimits_of_map_exact {A : Type u₁} {B : Type u₂} (L : A B) (h : ⦃X Y Z : A⦄ {f : X Y} {g : Y Z}, category_theory.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.

Equations
noncomputable def category_theory.functor.preserves_finite_limits_of_preserves_monos_and_cokernels {A : Type u₁} {B : Type u₂} (L : A B) [Π {X Y : A} (f : X Y), ] :

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

Equations
noncomputable def category_theory.functor.preserves_finite_colimits_of_preserves_epis_and_kernels {A : Type u₁} {B : Type u₂} (L : A B) [Π {X Y : A} (f : X Y), ] :

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

Equations