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

• A short complex S is exact iff imageSubobject S.f = kernelSubobject S.g.
• If (f, g) is exact, then image.ι f has the universal property of the kernel of g.
• f is a monomorphism iff kernel.ι f = 0 iff Exact 0 f, and f is an epimorphism iff cokernel.π = 0 iff Exact f 0.
• A faithful functor between abelian categories that preserves zero morphisms reflects exact sequences.
• X ⟶ Y ⟶ Z ⟶ 0 is exact if and only if the second map is a cokernel of the first, and 0 ⟶ X ⟶ Y ⟶ Z is exact if and only if the first map is a kernel of the second.
• A functor F such that for all S, we have S.Exact → (S.map F).Exact preserves both finite limits and colimits.

theorem CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel' {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] (S : ShortComplex C) : S.Exact ↔ Epi (imageToKernel' S.f S.g ⋯)

theorem CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] (S : ShortComplex C) : S.Exact ↔ Epi (imageToKernel S.f S.g ⋯)

theorem CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] (S : ShortComplex C) : S.Exact ↔ IsIso (imageToKernel S.f S.g ⋯)

theorem CategoryTheory.ShortComplex.exact_iff_image_eq_kernel {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] (S : ShortComplex C) : S.Exact ↔ Limits.imageSubobject S.f = Limits.kernelSubobject S.g

In an abelian category, a short complex S is exact iff imageSubobject S.f = kernelSubobject S.g.

theorem CategoryTheory.ShortComplex.exact_iff_of_forks {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] (S : ShortComplex C) {cg : Limits.KernelFork S.g} (hg : Limits.IsLimit cg) {cf : Limits.CokernelCofork S.f} (hf : Limits.IsColimit cf) : S.Exact ↔ CategoryStruct.comp (Limits.Fork.ι cg) (Limits.Cofork.π cf) = 0

def CategoryTheory.ShortComplex.Exact.isLimitImage {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {S : ShortComplex C} (h : S.Exact) : Limits.IsLimit (Limits.KernelFork.ofι (Abelian.image.ι S.f) ⋯)

If (f, g) is exact, then Abelian.image.ι S.f is a kernel of S.g.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.ShortComplex.Exact.isLimitImage' {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {S : ShortComplex C} (h : S.Exact) : Limits.IsLimit (Limits.KernelFork.ofι (Limits.image.ι S.f) ⋯)

If (f, g) is exact, then image.ι f is a kernel of g.

Equations

• h.isLimitImage' = CategoryTheory.Limits.IsKernel.isoKernel S.g (CategoryTheory.Limits.Image.monoFactorisation S.f).m h.isLimitImage (CategoryTheory.Abelian.imageIsoImage S.f).symm ⋯

def CategoryTheory.ShortComplex.Exact.isColimitCoimage {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {S : ShortComplex C} (h : S.Exact) : Limits.IsColimit (Limits.CokernelCofork.ofπ (Abelian.coimage.π S.g) ⋯)

If (f, g) is exact, then Abelian.coimage.π g is a cokernel of f.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.ShortComplex.Exact.isColimitImage {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {S : ShortComplex C} (h : S.Exact) : Limits.IsColimit (Limits.CokernelCofork.ofπ (Limits.factorThruImage S.g) ⋯)

If (f, g) is exact, then factorThruImage g is a cokernel of f.

Equations

• h.isColimitImage = CategoryTheory.Limits.IsCokernel.cokernelIso S.f (CategoryTheory.Limits.factorThruImage S.g) h.isColimitCoimage (CategoryTheory.Abelian.coimageIsoImage' S.g) ⋯

theorem CategoryTheory.ShortComplex.exact_kernel {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (mk (Limits.kernel.ι f) f ⋯).Exact

theorem CategoryTheory.ShortComplex.exact_cokernel {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {X Y : C} (f : X ⟶ Y) : (mk f (Limits.cokernel.π f) ⋯).Exact

theorem CategoryTheory.ShortComplex.exact_iff_exact_image_ι {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] (S : ShortComplex C) : S.Exact ↔ (mk (Abelian.image.ι S.f) S.g ⋯).Exact

theorem CategoryTheory.ShortComplex.exact_iff_exact_coimage_π {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] (S : ShortComplex C) : S.Exact ↔ (mk S.f (Abelian.coimage.π S.g) ⋯).Exact

theorem CategoryTheory.Abelian.tfae_mono {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {X Y : C} (f : X ⟶ Y) (Z : C) : [Mono f, Limits.kernel.ι f = 0, (ShortComplex.mk 0 f ⋯).Exact].TFAE

theorem CategoryTheory.Abelian.tfae_epi {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {X Y : C} (f : X ⟶ Y) (Z : C) : [Epi f, Limits.cokernel.π f = 0, (ShortComplex.mk f 0 ⋯).Exact].TFAE

theorem CategoryTheory.Functor.reflects_exact_of_faithful {C : Type u₁} [Category.{v₁, u₁} C] [Abelian C] {D : Type u₂} [Category.{v₂, u₂} D] [Abelian D] (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] (S : ShortComplex C) (hS : (S.map F).Exact) : S.Exact

theorem CategoryTheory.Functor.preservesMonomorphisms_of_map_exact {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Abelian A] [Abelian B] (L : Functor A B) [L.PreservesZeroMorphisms] (hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact) : L.PreservesMonomorphisms

A functor which preserves exactness preserves monomorphisms.

theorem CategoryTheory.Functor.preservesEpimorphisms_of_map_exact {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Abelian A] [Abelian B] (L : Functor A B) [L.PreservesZeroMorphisms] (hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact) : L.PreservesEpimorphisms

A functor which preserves exactness preserves epimorphisms.

theorem CategoryTheory.Functor.preservesHomology_of_map_exact {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Abelian A] [Abelian B] (L : Functor A B) [L.PreservesZeroMorphisms] (hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact) : L.PreservesHomology

A functor which preserves the exactness of short complexes preserves homology.

theorem CategoryTheory.Functor.preservesHomology_of_preservesMonos_and_cokernels {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Abelian A] [Abelian B] (L : Functor A B) [L.PreservesZeroMorphisms] [L.PreservesMonomorphisms] [∀ {X Y : A} (f : X ⟶ Y), Limits.PreservesColimit (Limits.parallelPair f 0) L] : L.PreservesHomology

A functor preserving zero morphisms, monos, and cokernels preserves homology.

theorem CategoryTheory.Functor.preservesHomology_of_preservesEpis_and_kernels {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Abelian A] [Abelian B] (L : Functor A B) [L.PreservesZeroMorphisms] [L.PreservesEpimorphisms] [∀ {X Y : A} (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) L] : L.PreservesHomology

A functor preserving zero morphisms, epis, and kernels preserves homology.