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 : C} {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 : C} {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 : C} {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 : C} {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]

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.

def CategoryTheory.Functor.preservesHomologyOfMapExact {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.

Equations

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

Instances For

@[deprecated CategoryTheory.Functor.PreservesHomology.preservesKernels]

def CategoryTheory.Functor.preservesKernelsOfMapExact {C : Type u_1} {D : Type u_2} :

{inst : CategoryTheory.Category.{u_3, u_1} C} → {inst_1 : CategoryTheory.Category.{u_4, u_2} D} → {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} → {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} → {F : CategoryTheory.Functor C D} → {inst_4 : 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

Equations

@CategoryTheory.Functor.preservesKernelsOfMapExact = @CategoryTheory.Functor.PreservesHomology.preservesKernels

Instances For

@[deprecated CategoryTheory.Functor.PreservesHomology.preservesCokernels]

def CategoryTheory.Functor.preservesCokernelsOfMapExact {C : Type u_1} {D : Type u_2} :

{inst : CategoryTheory.Category.{u_3, u_1} C} → {inst_1 : CategoryTheory.Category.{u_4, u_2} D} → {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} → {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} → {F : CategoryTheory.Functor C D} → {inst_4 : 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

Equations

@CategoryTheory.Functor.preservesCokernelsOfMapExact = @CategoryTheory.Functor.PreservesHomology.preservesCokernels

Instances For

def CategoryTheory.Functor.preservesHomologyOfPreservesMonosAndCokernels {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.

Equations

L.preservesHomologyOfPreservesMonosAndCokernels = L.preservesHomologyOfMapExact ⋯

Instances For

def CategoryTheory.Functor.preservesHomologyOfPreservesEpisAndKernels {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.

Equations

L.preservesHomologyOfPreservesEpisAndKernels = L.preservesHomologyOfMapExact ⋯

Instances For