Documentation

Mathlib.CategoryTheory.Abelian.Exact

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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :

S.Exact ↔ CategoryTheory.Epi (imageToKernel' S.f S.g ⋯)

theorem CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :

S.Exact ↔ CategoryTheory.Epi (imageToKernel S.f S.g ⋯)

theorem CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :

S.Exact ↔ CategoryTheory.IsIso (imageToKernel S.f S.g ⋯)

theorem CategoryTheory.ShortComplex.exact_iff_image_eq_kernel {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :

S.Exact ↔ CategoryTheory.Limits.imageSubobject S.f = CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) {cg : CategoryTheory.Limits.KernelFork S.g} (hg : CategoryTheory.Limits.IsLimit cg) {cf : CategoryTheory.Limits.CokernelCofork S.f} (hf : CategoryTheory.Limits.IsColimit cf) :

S.Exact ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι cg) (CategoryTheory.Limits.Cofork.π cf) = 0

def CategoryTheory.ShortComplex.Exact.isLimitImage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (h : S.Exact) :

CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.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

def CategoryTheory.ShortComplex.Exact.isLimitImage' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (h : S.Exact) :

CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.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

def CategoryTheory.ShortComplex.Exact.isColimitCoimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (h : S.Exact) :

CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.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

def CategoryTheory.ShortComplex.Exact.isColimitImage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (h : S.Exact) :

CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.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

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

(CategoryTheory.ShortComplex.mk (CategoryTheory.Limits.kernel.ι f) f ⋯).Exact

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

(CategoryTheory.ShortComplex.mk f (CategoryTheory.Limits.cokernel.π f) ⋯).Exact

theorem CategoryTheory.ShortComplex.exact_iff_exact_image_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :

S.Exact ↔ (CategoryTheory.ShortComplex.mk (CategoryTheory.Abelian.image.ι S.f) S.g ⋯).Exact

theorem CategoryTheory.ShortComplex.exact_iff_exact_coimage_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex C) :

S.Exact ↔ (CategoryTheory.ShortComplex.mk S.f (CategoryTheory.Abelian.coimage.π S.g) ⋯).Exact

theorem CategoryTheory.Abelian.tfae_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) (Z : C) :

[CategoryTheory.Mono f, CategoryTheory.Limits.kernel.ι f = 0, (CategoryTheory.ShortComplex.mk 0 f ⋯).Exact].TFAE

theorem CategoryTheory.Abelian.tfae_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) (Z : C) :

[CategoryTheory.Epi f, CategoryTheory.Limits.cokernel.π f = 0, (CategoryTheory.ShortComplex.mk f 0 ⋯).Exact].TFAE

theorem CategoryTheory.Functor.reflects_exact_of_faithful {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) [F.PreservesZeroMorphisms] [F.Faithful] (S : CategoryTheory.ShortComplex C) (hS : (S.map F).Exact) :

S.Exact

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

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

(S.map F).Exact

Alias of CategoryTheory.ShortComplex.Exact.map.

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) [L.PreservesZeroMorphisms] (hL : ∀ (S : CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian A] [CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B) [L.PreservesZeroMorphisms] (hL : ∀ (S : CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian A] [CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B) [L.PreservesZeroMorphisms] (hL : ∀ (S : CategoryTheory.ShortComplex A), S.Exact → (S.map L).Exact) :

L.PreservesHomology

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

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

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

CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F

Alias of CategoryTheory.Functor.PreservesHomology.preservesKernels.

the functor preserves kernels

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

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

CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F

Alias of CategoryTheory.Functor.PreservesHomology.preservesCokernels.

the functor preserves cokernels

theorem CategoryTheory.Functor.preservesHomology_of_preservesMonos_and_cokernels {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) [L.PreservesZeroMorphisms] [L.PreservesMonomorphisms] [∀ {X Y : A} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian A] [CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B) [L.PreservesZeroMorphisms] [L.PreservesEpimorphisms] [∀ {X Y : A} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) L] :

L.PreservesHomology

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