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.- 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
CategoryTheory.Abelian.exact_iff_image_eq_kernel
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{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 imageSubobject f = kernelSubobject g.
theorem
CategoryTheory.Abelian.exact_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
theorem
CategoryTheory.Abelian.exact_iff'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
{cg : CategoryTheory.Limits.KernelFork g}
(hg : CategoryTheory.Limits.IsLimit cg)
{cf : CategoryTheory.Limits.CokernelCofork f}
(hf : CategoryTheory.Limits.IsColimit cf)
:
theorem
CategoryTheory.Abelian.exact_tfae
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
theorem
CategoryTheory.Abelian.IsEquivalence.exact_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
{D : Type u₁}
[CategoryTheory.Category.{v₁, u₁} D]
[CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsEquivalence F]
:
CategoryTheory.Exact (F.map f) (F.map g) ↔ CategoryTheory.Exact f g
theorem
CategoryTheory.Abelian.exact_epi_comp_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
{W : C}
(h : W ⟶ X)
[CategoryTheory.Epi h]
:
The dual result is true even in non-abelian categories, see
CategoryTheory.exact_comp_mono_iff.
def
CategoryTheory.Abelian.isLimitImage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : CategoryTheory.Exact f g)
:
If (f, g) is exact, then Abelian.image.ι f is a kernel of g.
Instances For
def
CategoryTheory.Abelian.isLimitImage'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : CategoryTheory.Exact f g)
:
If (f, g) is exact, then image.ι f is a kernel of g.
Instances For
def
CategoryTheory.Abelian.isColimitCoimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : CategoryTheory.Exact f g)
:
If (f, g) is exact, then Abelian.coimage.π g is a cokernel of f.
Instances For
def
CategoryTheory.Abelian.isColimitImage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : CategoryTheory.Exact f g)
:
If (f, g) is exact, then factorThruImage g is a cokernel of f.
Instances For
theorem
CategoryTheory.Abelian.exact_cokernel
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Abelian.mono_cokernel_desc_of_exact
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : CategoryTheory.Exact f g)
:
theorem
CategoryTheory.Abelian.isIso_cokernel_desc_of_exact_of_epi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(ex : CategoryTheory.Exact f g)
[CategoryTheory.Epi g]
:
If ex : Exact f g and epi g, then cokernel.desc _ _ ex.w is an isomorphism.
theorem
CategoryTheory.Abelian.cokernel.desc.inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Epi g]
(ex : CategoryTheory.Exact f g)
{Z : C}
(h : CategoryTheory.Limits.cokernel f ⟶ Z)
:
theorem
CategoryTheory.Abelian.cokernel.desc.inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Epi g]
(ex : CategoryTheory.Exact f g)
:
let_fun this :=
(_ : CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.desc f g (_ : CategoryTheory.CategoryStruct.comp f g = 0)));
CategoryTheory.CategoryStruct.comp g
(CategoryTheory.inv (CategoryTheory.Limits.cokernel.desc f g (_ : CategoryTheory.CategoryStruct.comp f g = 0))) = CategoryTheory.Limits.cokernel.π f
theorem
CategoryTheory.Abelian.isIso_kernel_lift_of_exact_of_mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(ex : CategoryTheory.Exact f g)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.Abelian.kernel.lift.inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Mono f]
(ex : CategoryTheory.Exact f g)
{Z : C}
(h : Y ⟶ Z)
:
theorem
CategoryTheory.Abelian.kernel.lift.inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Mono f]
(ex : CategoryTheory.Exact f g)
:
let_fun this :=
(_ : CategoryTheory.IsIso (CategoryTheory.Limits.kernel.lift g f (_ : CategoryTheory.CategoryStruct.comp f g = 0)));
CategoryTheory.CategoryStruct.comp
(CategoryTheory.inv (CategoryTheory.Limits.kernel.lift g f (_ : CategoryTheory.CategoryStruct.comp f g = 0))) f = CategoryTheory.Limits.kernel.ι g
def
CategoryTheory.Abelian.isColimitOfExactOfEpi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Epi g]
(h : CategoryTheory.Exact f g)
:
If X ⟶ Y ⟶ Z ⟶ 0 is exact, then the second map is a cokernel of the first.
Instances For
def
CategoryTheory.Abelian.isLimitOfExactOfMono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Mono f]
(h : CategoryTheory.Exact f g)
:
If 0 ⟶ X ⟶ Y ⟶ Z is exact, then the first map is a kernel of the second.
Instances For
theorem
CategoryTheory.Abelian.exact_of_is_cokernel
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(w : CategoryTheory.CategoryStruct.comp f g = 0)
(h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g w))
:
theorem
CategoryTheory.Abelian.exact_of_is_kernel
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(w : CategoryTheory.CategoryStruct.comp f g = 0)
(h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f w))
:
theorem
CategoryTheory.Abelian.exact_iff_exact_image_ι
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
theorem
CategoryTheory.Abelian.exact_iff_exact_coimage_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
theorem
CategoryTheory.Abelian.tfae_mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(Z : C)
(f : X ⟶ Y)
:
theorem
CategoryTheory.Abelian.mono_iff_kernel_ι_eq_zero
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Abelian.tfae_epi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(Z : C)
(f : X ⟶ Y)
:
theorem
CategoryTheory.Abelian.epi_iff_cokernel_π_eq_zero
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.Abelian.Exact.op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : CategoryTheory.Exact f g)
:
CategoryTheory.Exact g.op f.op
theorem
CategoryTheory.Abelian.Exact.op_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
:
CategoryTheory.Exact g.op f.op ↔ CategoryTheory.Exact f g
theorem
CategoryTheory.Abelian.Exact.unop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{Z : Cᵒᵖ}
(g : X ⟶ Y)
(f : Y ⟶ Z)
(h : CategoryTheory.Exact g f)
:
CategoryTheory.Exact f.unop g.unop
theorem
CategoryTheory.Abelian.Exact.unop_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{Z : Cᵒᵖ}
(g : X ⟶ Y)
(f : Y ⟶ Z)
:
CategoryTheory.Exact f.unop g.unop ↔ CategoryTheory.Exact g f
instance
CategoryTheory.Functor.reflectsExactSequencesOfPreservesZeroMorphismsOfFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Abelian C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Faithful F]
:
theorem
CategoryTheory.Functor.map_exact
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
[CategoryTheory.Limits.PreservesFiniteLimits L]
[CategoryTheory.Limits.PreservesFiniteColimits L]
{X : A}
{Y : A}
{Z : A}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(e1 : CategoryTheory.Exact f g)
:
CategoryTheory.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.preservesFiniteLimitsOfMapExact and
Functor.preservesFiniteColimitsOfMapExact.
theorem
CategoryTheory.Functor.preservesZeroMorphisms_of_map_exact
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g))
:
A functor which preserves exactness preserves zero morphisms.
theorem
CategoryTheory.Functor.preservesMonomorphisms_of_map_exact
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g))
:
A functor which preserves exactness preserves monomorphisms.
theorem
CategoryTheory.Functor.preservesEpimorphisms_of_map_exact
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g))
:
A functor which preserves exactness preserves epimorphisms.
def
CategoryTheory.Functor.preservesKernelsOfMapExact
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g))
(X : A)
(Y : A)
(f : X ⟶ Y)
:
A functor which preserves exactness preserves kernels.
Instances For
def
CategoryTheory.Functor.preservesCokernelsOfMapExact
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g))
(X : A)
(Y : A)
(f : X ⟶ Y)
:
A functor which preserves exactness preserves zero cokernels.
Instances For
def
CategoryTheory.Functor.preservesFiniteLimitsOfMapExact
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.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.
Instances For
def
CategoryTheory.Functor.preservesFiniteColimitsOfMapExact
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
(h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.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.
Instances For
def
CategoryTheory.Functor.preservesFiniteLimitsOfPreservesMonosAndCokernels
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
[CategoryTheory.Functor.PreservesZeroMorphisms L]
[CategoryTheory.Functor.PreservesMonomorphisms L]
[{X Y : A} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) L]
:
A functor preserving zero morphisms, monos, and cokernels preserves finite limits.
Instances For
def
CategoryTheory.Functor.preservesFiniteColimitsOfPreservesEpisAndKernels
{A : Type u₁}
{B : Type u₂}
[CategoryTheory.Category.{v₁, u₁} A]
[CategoryTheory.Category.{v₂, u₂} B]
[CategoryTheory.Abelian A]
[CategoryTheory.Abelian B]
(L : CategoryTheory.Functor A B)
[CategoryTheory.Functor.PreservesZeroMorphisms L]
[CategoryTheory.Functor.PreservesEpimorphisms L]
[{X Y : A} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) L]
:
A functor preserving zero morphisms, epis, and kernels preserves finite colimits.