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.

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

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

category_theory.exact (F.map f) (F.map g) ↔ category_theory.exact f g

source

theorem category_theory.abelian.exact_epi_comp_iff {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {W : C} (h : W ⟶ X) [category_theory.epi h] :

category_theory.exact (h ≫ f) g ↔ category_theory.exact f g

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

source

noncomputable 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.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 h = category_theory.limits.is_limit.of_ι (category_theory.abelian.image.ι f) _ (λ (W : C) (u : W ⟶ Y) (hu : u ≫ g = 0), category_theory.limits.kernel.lift (category_theory.limits.cokernel.π f) u _) _ _

source

noncomputable 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 h = category_theory.limits.is_kernel.iso_kernel g (category_theory.limits.image.ι f) (category_theory.abelian.is_limit_image f g h) (category_theory.abelian.image_iso_image f).symm _

source

noncomputable 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.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 h = category_theory.limits.is_colimit.of_π (category_theory.abelian.coimage.π g) _ (λ (W : C) (u : Y ⟶ W) (hu : f ≫ u = 0), category_theory.limits.cokernel.desc (category_theory.limits.kernel.ι g) u _) _ _

source

noncomputable 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 h = category_theory.limits.is_cokernel.cokernel_iso f (category_theory.limits.factor_thru_image g) (category_theory.abelian.is_colimit_coimage f g h) (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

@[protected, 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) (h : category_theory.exact f g) :

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

source

@[protected, instance]

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

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

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

source

@[simp]

theorem category_theory.abelian.cokernel.desc.inv_assoc {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.epi g] (ex : category_theory.exact f g) {X' : C} (f' : category_theory.limits.cokernel f ⟶ X') :

g ≫ category_theory.inv (category_theory.limits.cokernel.desc f g _) ≫ f' = category_theory.limits.cokernel.π f ≫ f'

source

@[simp]

theorem category_theory.abelian.cokernel.desc.inv {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.epi g] (ex : category_theory.exact f g) :

g ≫ category_theory.inv (category_theory.limits.cokernel.desc f g _) = category_theory.limits.cokernel.π f

source

@[protected, instance]

def category_theory.abelian.category_theory.limits.kernel.lift.category_theory.is_iso {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (ex : category_theory.exact f g) [category_theory.mono f] :

category_theory.is_iso (category_theory.limits.kernel.lift g f _)

source

@[simp]

theorem category_theory.abelian.kernel.lift.inv_assoc {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.mono f] (ex : category_theory.exact f g) {X' : C} (f' : Y ⟶ X') :

category_theory.inv (category_theory.limits.kernel.lift g f _) ≫ f ≫ f' = category_theory.limits.kernel.ι g ≫ f'

source

@[simp]

theorem category_theory.abelian.kernel.lift.inv {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.mono f] (ex : category_theory.exact f g) :

category_theory.inv (category_theory.limits.kernel.lift g f _) ≫ f = category_theory.limits.kernel.ι g

source

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

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

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

Equations

category_theory.abelian.is_colimit_of_exact_of_epi f g h = (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair f 0)).of_iso_colimit (category_theory.limits.cocones.ext {hom := category_theory.limits.cokernel.desc f g _, inv := category_theory.abelian.epi_desc g (category_theory.limits.cokernel.π f) _, hom_inv_id' := _, inv_hom_id' := _} _)

source

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

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

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

Equations

category_theory.abelian.is_limit_of_exact_of_mono f g h = (category_theory.limits.limit.is_limit (category_theory.limits.parallel_pair g 0)).of_iso_limit (category_theory.limits.cones.ext {hom := category_theory.abelian.mono_lift f (category_theory.limits.kernel.ι g) _, inv := category_theory.limits.kernel.lift g f _, hom_inv_id' := _, inv_hom_id' := _} _)

source

theorem category_theory.abelian.exact_of_is_cokernel {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) (h : category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π g w)) :

category_theory.exact f g

source

theorem category_theory.abelian.exact_of_is_kernel {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) (h : category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι f w)) :

category_theory.exact 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

source

theorem category_theory.abelian.exact.op {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.exact g.op f.op

source

theorem category_theory.abelian.exact.op_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 g.op f.op ↔ category_theory.exact f g

source

theorem category_theory.abelian.exact.unop {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : Cᵒᵖ} (g : X ⟶ Y) (f : Y ⟶ Z) (h : category_theory.exact g f) :

category_theory.exact f.unop g.unop

source

theorem category_theory.abelian.exact.unop_iff {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {X Y Z : Cᵒᵖ} (g : X ⟶ Y) (f : Y ⟶ Z) :

category_theory.exact f.unop g.unop ↔ category_theory.exact g f

source

@[protected, instance]

def category_theory.functor.reflects_exact_sequences_of_preserves_zero_morphisms_of_faithful {C : Type u₁} [category_theory.category C] [category_theory.abelian C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) [F.preserves_zero_morphisms] [category_theory.faithful F] :

F.reflects_exact_sequences

Equations

F.reflects_exact_sequences_of_preserves_zero_morphisms_of_faithful = {reflects := _}