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 C] [Abelian C] (S : ShortComplex C) : Iff S.Exact (Epi (imageToKernel' S.f S.g ⋯))

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

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

theorem CategoryTheory.ShortComplex.exact_iff_image_eq_kernel {C : Type u₁} [Category C] [Abelian C] (S : ShortComplex C) : Iff S.Exact (Eq (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 C] [Abelian C] (S : ShortComplex C) {cg : Limits.KernelFork S.g} (hg : Limits.IsLimit cg) {cf : Limits.CokernelCofork S.f} (hf : Limits.IsColimit cf) : Iff S.Exact (Eq (CategoryStruct.comp (Limits.Fork.ι cg) (Limits.Cofork.π cf)) 0)

def CategoryTheory.ShortComplex.Exact.isLimitImage {C : Type u₁} [Category 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 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

• Eq 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 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 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

• Eq 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 C] [Abelian C] {X Y : C} (f : Quiver.Hom X Y) : { X₁ := Limits.kernel f, X₂ := X, X₃ := Y, f := Limits.kernel.ι f, g := f, zero := ⋯ }.Exact

theorem CategoryTheory.ShortComplex.exact_cokernel {C : Type u₁} [Category C] [Abelian C] {X Y : C} (f : Quiver.Hom X Y) : { X₁ := X, X₂ := Y, X₃ := Limits.cokernel f, f := f, g := Limits.cokernel.π f, zero := ⋯ }.Exact

theorem CategoryTheory.ShortComplex.exact_iff_exact_image_ι {C : Type u₁} [Category C] [Abelian C] (S : ShortComplex C) : Iff S.Exact { X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ }.Exact

theorem CategoryTheory.ShortComplex.exact_iff_exact_coimage_π {C : Type u₁} [Category C] [Abelian C] (S : ShortComplex C) : Iff S.Exact { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }.Exact

theorem CategoryTheory.Abelian.tfae_mono {C : Type u₁} [Category C] [Abelian C] {X Y : C} (f : Quiver.Hom X Y) (Z : C) : (List.cons (Mono f) (List.cons (Eq (Limits.kernel.ι f) 0) (List.cons { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.Exact List.nil))).TFAE

theorem CategoryTheory.Abelian.tfae_epi {C : Type u₁} [Category C] [Abelian C] {X Y : C} (f : Quiver.Hom X Y) (Z : C) : (List.cons (Epi f) (List.cons (Eq (Limits.cokernel.π f) 0) (List.cons { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := 0, zero := ⋯ }.Exact List.nil))).TFAE

theorem CategoryTheory.Functor.reflects_exact_of_faithful {C : Type u₁} [Category C] [Abelian C] {D : Type u₂} [Category 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 A] [Category 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 A] [Category 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 A] [Category 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 A] [Category B] [Abelian A] [Abelian B] (L : Functor A B) [L.PreservesZeroMorphisms] [L.PreservesMonomorphisms] [∀ {X Y : A} (f : Quiver.Hom 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 A] [Category B] [Abelian A] [Abelian B] (L : Functor A B) [L.PreservesZeroMorphisms] [L.PreservesEpimorphisms] [∀ {X Y : A} (f : Quiver.Hom X Y), Limits.PreservesLimit (Limits.parallelPair f 0) L] : L.PreservesHomology

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