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.

source

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 ⋯)

source

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 ⋯)

source

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 ⋯)

source

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.

source

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

source

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.

Instances For

source

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 ⋯

Instances For

source

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.

Instances For

source

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) ⋯

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[deprecated CategoryTheory.ShortComplex.Exact.map (since := "2024-07-09")]

theorem CategoryTheory.Functor.CategoryTheory.Functor.map_exact {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S : ShortComplex C} (h : S.Exact) (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :

(S.map F).Exact

Alias of CategoryTheory.ShortComplex.Exact.map.

source

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.

source

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.

source

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.

source

@[deprecated CategoryTheory.Functor.PreservesHomology.preservesKernels (since := "2024-07-09")]

theorem CategoryTheory.Functor.preservesKernelsOfMapExact {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : Limits.HasZeroMorphisms C} {inst✝³ : Limits.HasZeroMorphisms D} {F : Functor C D} {inst✝⁴ : F.PreservesZeroMorphisms} [self : F.PreservesHomology] ⦃X Y : C⦄ (f : X ⟶ Y) :

Limits.PreservesLimit (Limits.parallelPair f 0) F

Alias of CategoryTheory.Functor.PreservesHomology.preservesKernels.

the functor preserves kernels

source

@[deprecated CategoryTheory.Functor.PreservesHomology.preservesCokernels (since := "2024-07-09")]

theorem CategoryTheory.Functor.preservesCokernelsOfMapExact {C : Type u_1} {D : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} D} {inst✝² : Limits.HasZeroMorphisms C} {inst✝³ : Limits.HasZeroMorphisms D} {F : Functor C D} {inst✝⁴ : F.PreservesZeroMorphisms} [self : F.PreservesHomology] ⦃X Y : C⦄ (f : X ⟶ Y) :

Limits.PreservesColimit (Limits.parallelPair f 0) F

Alias of CategoryTheory.Functor.PreservesHomology.preservesCokernels.

the functor preserves cokernels

source

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.

source

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.

Documentation

Mathlib.CategoryTheory.Abelian.Exact

Exact sequences in abelian categories #

Main results #