Exact sequences in abelian categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.- A faithful functor between abelian categories that preserves zero morphisms reflects exact sequences.
X ⟶ Y ⟶ Z ⟶ 0is exact if and only if the second map is a cokernel of the first, and0 ⟶ X ⟶ Y ⟶ Zis exact if and only if the first map is a kernel of the second.- An exact functor preserves exactness, more specifically,
Fpreserves finite colimits and finite limits, if and only ifexact f gimpliesexact (F.map f) (F.map g).
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) :
In an abelian category, a pair of morphisms f : X ⟶ Y, g : Y ⟶ Z is exact
iff image_subobject f = kernel_subobject g.
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
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) :
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
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_comp_mono_iff.
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) :
If (f, g) is exact, then abelian.image.ι f is a kernel of g.
Equations
- category_theory.abelian.is_limit_image f g h = category_theory.limits.kernel_fork.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 _) _ _
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) :
If (f, g) is exact, then image.ι f is a kernel of g.
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) :
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.cokernel_cofork.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 _) _ _
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) :
If (f, g) is exact, then factor_thru_image g is a cokernel of f.
theorem
category_theory.abelian.exact_cokernel
{C : Type u₁}
[category_theory.category C]
[category_theory.abelian C]
{X Y : C}
(f : X ⟶ Y) :
@[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) :
@[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] :
If ex : exact f g and epi g, then cokernel.desc _ _ ex.w is an isomorphism.
@[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'
@[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) :
@[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] :
@[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'
@[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) :
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) :
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' := _} _)
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) :
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' := _} _)
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)) :
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)) :
theorem
category_theory.abelian.exact_iff_exact_image_ι
{C : Type u₁}
[category_theory.category C]
[category_theory.abelian C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
theorem
category_theory.abelian.exact_iff_exact_coimage_π
{C : Type u₁}
[category_theory.category C]
[category_theory.abelian C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
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_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_cokernel_π_eq_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.abelian C]
{X Y : C}
(f : X ⟶ Y) :
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) :
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
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) :
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) :
@[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] :
Equations
theorem
category_theory.functor.map_exact
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
[category_theory.limits.preserves_finite_limits L]
[category_theory.limits.preserves_finite_colimits L]
{X Y Z : A}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(e1 : category_theory.exact f g) :
category_theory.exact (L.map f) (L.map g)
A functor preserving finite limits and finite colimits preserves exactness. The converse
result is also true, see functor.preserves_finite_limits_of_map_exact and
functor.preserves_finite_colimits_of_map_exact.
theorem
category_theory.functor.preserves_zero_morphisms_of_map_exact
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, category_theory.exact f g → category_theory.exact (L.map f) (L.map g)) :
A functor which preserves exactness preserves zero morphisms.
theorem
category_theory.functor.preserves_monomorphisms_of_map_exact
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, category_theory.exact f g → category_theory.exact (L.map f) (L.map g)) :
A functor which preserves exactness preserves monomorphisms.
theorem
category_theory.functor.preserves_epimorphisms_of_map_exact
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, category_theory.exact f g → category_theory.exact (L.map f) (L.map g)) :
A functor which preserves exactness preserves epimorphisms.
noncomputable
def
category_theory.functor.preserves_kernels_of_map_exact
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, category_theory.exact f g → category_theory.exact (L.map f) (L.map g))
(X Y : A)
(f : X ⟶ Y) :
A functor which preserves exactness preserves kernels.
Equations
- L.preserves_kernels_of_map_exact h X Y f = {preserves := λ (c : category_theory.limits.cone (category_theory.limits.parallel_pair f 0)) (ic : category_theory.limits.is_limit c), let _inst : L.preserves_zero_morphisms := _, _inst_1 : L.preserves_monomorphisms := _, _inst_2 : category_theory.mono (category_theory.limits.fork.ι c) := _ in (⇑((category_theory.limits.is_limit_map_cone_fork_equiv' L _).symm) (category_theory.abelian.is_limit_of_exact_of_mono (L.map (category_theory.limits.fork.ι c)) (L.map f) _)).of_iso_limit ((category_theory.limits.cones.functoriality (category_theory.limits.parallel_pair f 0) L).map_iso (category_theory.limits.iso_of_ι c).symm)}
noncomputable
def
category_theory.functor.preserves_cokernels_of_map_exact
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, category_theory.exact f g → category_theory.exact (L.map f) (L.map g))
(X Y : A)
(f : X ⟶ Y) :
A functor which preserves exactness preserves zero cokernels.
Equations
- L.preserves_cokernels_of_map_exact h X Y f = {preserves := λ (c : category_theory.limits.cocone (category_theory.limits.parallel_pair f 0)) (ic : category_theory.limits.is_colimit c), let _inst : L.preserves_zero_morphisms := _, _inst_1 : L.preserves_epimorphisms := _, _inst_2 : category_theory.epi (category_theory.limits.cofork.π c) := _ in (⇑((category_theory.limits.is_colimit_map_cocone_cofork_equiv' L _).symm) (category_theory.abelian.is_colimit_of_exact_of_epi (L.map f) (L.map (category_theory.limits.cofork.π c)) _)).of_iso_colimit ((category_theory.limits.cocones.functoriality (category_theory.limits.parallel_pair f 0) L).map_iso (category_theory.limits.iso_of_π c).symm)}
noncomputable
def
category_theory.functor.preserves_finite_limits_of_map_exact
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, category_theory.exact f g → category_theory.exact (L.map f) (L.map g)) :
A functor which preserves exactness is left exact, i.e. preserves finite limits.
This is part of the inverse implication to functor.map_exact.
Equations
- L.preserves_finite_limits_of_map_exact h = let _inst : L.preserves_zero_morphisms := _, _inst_1 : Π (X Y : A) (f : X ⟶ Y), category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) L := L.preserves_kernels_of_map_exact h in L.preserves_finite_limits_of_preserves_kernels
noncomputable
def
category_theory.functor.preserves_finite_colimits_of_map_exact
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, category_theory.exact f g → category_theory.exact (L.map f) (L.map g)) :
A functor which preserves exactness is right exact, i.e. preserves finite colimits.
This is part of the inverse implication to functor.map_exact.
Equations
- L.preserves_finite_colimits_of_map_exact h = let _inst : L.preserves_zero_morphisms := _, _inst_1 : Π (X Y : A) (f : X ⟶ Y), category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) L := L.preserves_cokernels_of_map_exact h in L.preserves_finite_colimits_of_preserves_cokernels
noncomputable
def
category_theory.functor.preserves_finite_limits_of_preserves_monos_and_cokernels
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
[L.preserves_zero_morphisms]
[L.preserves_monomorphisms]
[Π {X Y : A} (f : X ⟶ Y), category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) L] :
A functor preserving zero morphisms, monos, and cokernels preserves finite limits.
noncomputable
def
category_theory.functor.preserves_finite_colimits_of_preserves_epis_and_kernels
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.abelian A]
[category_theory.abelian B]
(L : A ⥤ B)
[L.preserves_zero_morphisms]
[L.preserves_epimorphisms]
[Π {X Y : A} (f : X ⟶ Y), category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) L] :
A functor preserving zero morphisms, epis, and kernels preserves finite colimits.