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.

source

theorem category_theory.abelian.exact_iff_image_eq_kernel {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :

category_theory.exact f g ↔ category_theory.limits.image_subobject f = category_theory.limits.kernel_subobject g

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

source

theorem category_theory.abelian.exact_iff {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :

category_theory.exact f g ↔ f ≫ g = 0 ∧ category_theory.limits.kernel.ι g ≫ category_theory.limits.cokernel.π f = 0

source

theorem category_theory.abelian.exact_iff' {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {cg : category_theory.limits.kernel_fork g} (hg : category_theory.limits.is_limit cg) {cf : category_theory.limits.cokernel_cofork f} (hf : category_theory.limits.is_colimit cf) :

category_theory.exact f g ↔ f ≫ g = 0 ∧ category_theory.limits.fork.ι cg ≫ category_theory.limits.cofork.π cf = 0

source

theorem category_theory.abelian.exact_tfae {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :

[category_theory.exact f g, f ≫ g = 0 ∧ category_theory.limits.kernel.ι g ≫ category_theory.limits.cokernel.π f = 0, category_theory.limits.image_subobject f = category_theory.limits.kernel_subobject g].tfae

source

def category_theory.abelian.is_limit_image {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : category_theory.exact f g] :

category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι (category_theory.abelian.images.image.ι f) _)

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

Equations

category_theory.abelian.is_limit_image f g = category_theory.limits.is_limit.of_ι (category_theory.abelian.images.image.ι f) _ (λ (W : C) (u : W ⟶ Y) (hu : u ≫ g = 0), category_theory.limits.kernel.lift (category_theory.limits.cokernel.π f) u _) _ _

source

def category_theory.abelian.is_limit_image' {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : category_theory.exact f g] :

category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι (category_theory.limits.image.ι f) _)

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

Equations

category_theory.abelian.is_limit_image' f g = category_theory.limits.is_kernel.iso_kernel g (category_theory.limits.image.ι f) (category_theory.abelian.is_limit_image f g) (category_theory.abelian.image_iso_image f).symm _

source

def category_theory.abelian.is_colimit_coimage {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : category_theory.exact f g] :

category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π (category_theory.abelian.coimages.coimage.π g) _)

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

Equations

category_theory.abelian.is_colimit_coimage f g = category_theory.limits.is_colimit.of_π (category_theory.abelian.coimages.coimage.π g) _ (λ (W : C) (u : Y ⟶ W) (hu : f ≫ u = 0), category_theory.limits.cokernel.desc (category_theory.limits.kernel.ι g) u _) _ _

source

def category_theory.abelian.is_colimit_image {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [h : category_theory.exact f g] :

category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π (category_theory.limits.factor_thru_image g) _)

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

Equations

category_theory.abelian.is_colimit_image f g = category_theory.limits.is_cokernel.cokernel_iso f (category_theory.limits.factor_thru_image g) (category_theory.abelian.is_colimit_coimage f g) (category_theory.abelian.coimage_iso_image' g) _

source

theorem category_theory.abelian.exact_cokernel {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :

category_theory.exact f (category_theory.limits.cokernel.π f)

source

@[instance]

def category_theory.abelian.category_theory.limits.cokernel.desc.category_theory.mono {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.exact f g] :

category_theory.mono (category_theory.limits.cokernel.desc f g _)

source

theorem category_theory.abelian.tfae_mono {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y : C} (Z : C) (f : X ⟶ Y) :

[category_theory.mono f, category_theory.limits.kernel.ι f = 0, category_theory.exact 0 f].tfae

source

theorem category_theory.abelian.mono_iff_kernel_ι_eq_zero {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :

category_theory.mono f ↔ category_theory.limits.kernel.ι f = 0

source

theorem category_theory.abelian.tfae_epi {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y : C} (Z : C) (f : X ⟶ Y) :

[category_theory.epi f, category_theory.limits.cokernel.π f = 0, category_theory.exact f 0].tfae

source

theorem category_theory.abelian.epi_iff_cokernel_π_eq_zero {C : Type u} [category_theory.category C] [category_theory.abelian C] {X Y : C} (f : X ⟶ Y) :

category_theory.epi f ↔ category_theory.limits.cokernel.π f = 0