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 = 0andkernel.ι 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.ι fhas the universal property of the kernel ofg. fis a monomorphism iffkernel.ι f = 0iffexact 0 f, andfis an epimorphism iffcokernel.π = 0iffexact f 0.
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
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
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] :
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 _) _ _
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] :
If (f, g) is exact, then image.ι f is a kernel of g.
theorem
category_theory.abelian.exact_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
{X Y : C}
(f : X ⟶ Y) :
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) :
theorem
category_theory.abelian.mono_iff_exact_zero_left
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
{X Y : C}
(Z : C)
(f : X ⟶ Y) :
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) :
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) :
theorem
category_theory.abelian.epi_iff_exact_zero_right
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
{X Y : C}
(Z : C)
(f : X ⟶ Y) :
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) :