Exact sequences in abelian categories
We prove that in an abelian category, (f, g) is exact if and only if f ≫ g = 0 and
kernel.ι g ≫ 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) :
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} :
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 image.ι f is a kernel of g.
Equations
- category_theory.abelian.is_limit_image f g = category_theory.limits.is_limit.of_ι (category_theory.limits.image.ι f) _ (λ (W : C) (u : W ⟶ Y) (hu : u ≫ g = 0), category_theory.limits.kernel.lift (category_theory.limits.cokernel.π f) u _) _ _