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) :