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 iff ≫ g = 0
andkernel.ι g ≫ cokernel.π f = 0
. This characterisation tends to be less cumbersome to work with than the original definition involving the comparison mapimage f ⟶ kernel g
.- If
(f, g)
is exact, thenimage.ι f
has the universal property of the kernel ofg
. f
is a monomorphism iffkernel.ι f = 0
iffexact 0 f
, andf
is an epimorphism iffcokernel.π = 0
iffexact 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, and0 ⟶ X ⟶ Y ⟶ Z
is exact if and only if the first map is a kernel of the second.
In an abelian category, a pair of morphisms f : X ⟶ Y
, g : Y ⟶ Z
is exact
iff image_subobject f = kernel_subobject g
.
The dual result is true even in non-abelian categories, see
category_theory.exact_epi_comp_iff
.
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 _) _ _
If (f, g)
is exact, then image.ι f
is a kernel of 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 _) _ _
If (f, g)
is exact, then factor_thru_image g
is a cokernel of f
.
If ex : exact f g
and epi g
, then cokernel.desc _ _ ex.w
is an isomorphism.
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' := _} _)
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' := _} _)