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 #

(f, g) is exact if and only if f ≫ g = 0 and kernel.ι g ≫ cokernel.π f = 0. This characterisation tends to be less cumbersome to work with than the original definition involving the comparison map image f ⟶ kernel 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.
An exact functor preserves exactness, more specifically, F preserves finite colimits and finite limits, if and only if Exact f g implies Exact (F.map f) (F.map g).

source

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

CategoryTheory.Exact f g ↔ CategoryTheory.Limits.imageSubobject f = CategoryTheory.Limits.kernelSubobject g

In an abelian category, a pair of morphisms f : X ⟶ Y, g : Y ⟶ Z is exact iff imageSubobject f = kernelSubobject g.

source

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

CategoryTheory.Exact f g ↔ CategoryTheory.CategoryStruct.comp f g = 0 ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.Limits.cokernel.π f) = 0

source

theorem CategoryTheory.Abelian.exact_iff' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {cg : CategoryTheory.Limits.KernelFork g} (hg : CategoryTheory.Limits.IsLimit cg) {cf : CategoryTheory.Limits.CokernelCofork f} (hf : CategoryTheory.Limits.IsColimit cf) :

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

source

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

List.TFAE [CategoryTheory.Exact f g, CategoryTheory.CategoryStruct.comp f g = 0 ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.Limits.cokernel.π f) = 0, CategoryTheory.Limits.imageSubobject f = CategoryTheory.Limits.kernelSubobject g]

source

theorem CategoryTheory.Abelian.IsEquivalence.exact_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsEquivalence F] :

CategoryTheory.Exact (F.toPrefunctor.map f) (F.toPrefunctor.map g) ↔ CategoryTheory.Exact f g

source

theorem CategoryTheory.Abelian.exact_epi_comp_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {W : C} (h : W ⟶ X) [CategoryTheory.Epi h] :

CategoryTheory.Exact (CategoryTheory.CategoryStruct.comp h f) g ↔ CategoryTheory.Exact f g

The dual result is true even in non-abelian categories, see CategoryTheory.exact_comp_mono_iff.

source

def CategoryTheory.Abelian.isLimitImage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryTheory.Exact f g) :

CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Abelian.image.ι f) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.image.ι f) g = 0))

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

Equations

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

Instances For

source

def CategoryTheory.Abelian.isLimitImage' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryTheory.Exact f g) :

CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.image.ι f) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) g = 0))

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

Equations

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

Instances For

source

def CategoryTheory.Abelian.isColimitCoimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryTheory.Exact f g) :

CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Abelian.coimage.π g) (_ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.coimage.π g) = 0))

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.Abelian.isColimitImage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryTheory.Exact f g) :

CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.factorThruImage g) (_ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.factorThruImage g) = 0))

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

Equations

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

Instances For

source

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

CategoryTheory.Exact f (CategoryTheory.Limits.cokernel.π f)

source

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

CategoryTheory.Mono (CategoryTheory.Limits.cokernel.desc f g (_ : CategoryTheory.CategoryStruct.comp f g = 0))

source

theorem CategoryTheory.Abelian.isIso_cokernel_desc_of_exact_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (ex : CategoryTheory.Exact f g) [CategoryTheory.Epi g] :

CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.desc f g (_ : CategoryTheory.CategoryStruct.comp f g = 0))

If ex : Exact f g and epi g, then cokernel.desc _ _ ex.w is an isomorphism.

source

theorem CategoryTheory.Abelian.cokernel.desc.inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z✝) [CategoryTheory.Epi g] (ex : CategoryTheory.Exact f g) {Z : C} (h : CategoryTheory.Limits.cokernel f ⟶ Z) :

CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.cokernel.desc f g (_ : CategoryTheory.CategoryStruct.comp f g = 0))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) h

source

theorem CategoryTheory.Abelian.cokernel.desc.inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Epi g] (ex : CategoryTheory.Exact f g) :

let_fun this := (_ : CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.desc f g (_ : CategoryTheory.CategoryStruct.comp f g = 0))); CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv (CategoryTheory.Limits.cokernel.desc f g (_ : CategoryTheory.CategoryStruct.comp f g = 0))) = CategoryTheory.Limits.cokernel.π f

source

theorem CategoryTheory.Abelian.isIso_kernel_lift_of_exact_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (ex : CategoryTheory.Exact f g) [CategoryTheory.Mono f] :

CategoryTheory.IsIso (CategoryTheory.Limits.kernel.lift g f (_ : CategoryTheory.CategoryStruct.comp f g = 0))

source

theorem CategoryTheory.Abelian.kernel.lift.inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z✝) [CategoryTheory.Mono f] (ex : CategoryTheory.Exact f g) {Z : C} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.kernel.lift g f (_ : CategoryTheory.CategoryStruct.comp f g = 0))) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) h

source

theorem CategoryTheory.Abelian.kernel.lift.inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Mono f] (ex : CategoryTheory.Exact f g) :

let_fun this := (_ : CategoryTheory.IsIso (CategoryTheory.Limits.kernel.lift g f (_ : CategoryTheory.CategoryStruct.comp f g = 0))); CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.kernel.lift g f (_ : CategoryTheory.CategoryStruct.comp f g = 0))) f = CategoryTheory.Limits.kernel.ι g

source

def CategoryTheory.Abelian.isColimitOfExactOfEpi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Epi g] (h : CategoryTheory.Exact f g) :

CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g (_ : CategoryTheory.CategoryStruct.comp f g = 0))

If X ⟶ Y ⟶ Z ⟶ 0 is exact, then the second map is a cokernel of the first.

Equations

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

Instances For

source

def CategoryTheory.Abelian.isLimitOfExactOfMono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Mono f] (h : CategoryTheory.Exact f g) :

CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f (_ : CategoryTheory.CategoryStruct.comp f g = 0))

If 0 ⟶ X ⟶ Y ⟶ Z is exact, then the first map is a kernel of the second.

Equations

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

Instances For

source

theorem CategoryTheory.Abelian.exact_of_is_cokernel {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g w)) :

CategoryTheory.Exact f g

source

theorem CategoryTheory.Abelian.exact_of_is_kernel {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (w : CategoryTheory.CategoryStruct.comp f g = 0) (h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f w)) :

CategoryTheory.Exact f g

source

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

CategoryTheory.Exact f g ↔ CategoryTheory.Exact (CategoryTheory.Abelian.image.ι f) g

source

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

CategoryTheory.Exact f g ↔ CategoryTheory.Exact f (CategoryTheory.Abelian.coimage.π g)

source

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

List.TFAE [CategoryTheory.Mono f, CategoryTheory.Limits.kernel.ι f = 0, CategoryTheory.Exact 0 f]

source

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

CategoryTheory.Mono f ↔ CategoryTheory.Limits.kernel.ι f = 0

source

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

List.TFAE [CategoryTheory.Epi f, CategoryTheory.Limits.cokernel.π f = 0, CategoryTheory.Exact f 0]

source

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

CategoryTheory.Epi f ↔ CategoryTheory.Limits.cokernel.π f = 0

source

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

CategoryTheory.Exact g.op f.op

source

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

CategoryTheory.Exact g.op f.op ↔ CategoryTheory.Exact f g

source

theorem CategoryTheory.Abelian.Exact.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (g : X ⟶ Y) (f : Y ⟶ Z) (h : CategoryTheory.Exact g f) :

CategoryTheory.Exact f.unop g.unop

source

theorem CategoryTheory.Abelian.Exact.unop_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} (g : X ⟶ Y) (f : Y ⟶ Z) :

CategoryTheory.Exact f.unop g.unop ↔ CategoryTheory.Exact g f

source

instance CategoryTheory.Functor.reflectsExactSequencesOfPreservesZeroMorphismsOfFaithful {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) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Faithful F] :

CategoryTheory.Functor.ReflectsExactSequences F

Equations

(_ : CategoryTheory.Functor.ReflectsExactSequences F) = (_ : CategoryTheory.Functor.ReflectsExactSequences F)

source

theorem CategoryTheory.Functor.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) [CategoryTheory.Limits.PreservesFiniteLimits L] [CategoryTheory.Limits.PreservesFiniteColimits L] {X : A} {Y : A} {Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (e1 : CategoryTheory.Exact f g) :

CategoryTheory.Exact (L.toPrefunctor.map f) (L.toPrefunctor.map g)

A functor preserving finite limits and finite colimits preserves exactness. The converse result is also true, see Functor.preservesFiniteLimitsOfMapExact and Functor.preservesFiniteColimitsOfMapExact.

source

theorem CategoryTheory.Functor.preservesZeroMorphisms_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) (h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.toPrefunctor.map f) (L.toPrefunctor.map g)) :

CategoryTheory.Functor.PreservesZeroMorphisms L

A functor which preserves exactness preserves zero morphisms.

source

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) (h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.toPrefunctor.map f) (L.toPrefunctor.map g)) :

CategoryTheory.Functor.PreservesMonomorphisms L

A functor which preserves exactness preserves monomorphisms.

source

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) (h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.toPrefunctor.map f) (L.toPrefunctor.map g)) :

CategoryTheory.Functor.PreservesEpimorphisms L

A functor which preserves exactness preserves epimorphisms.

source

def CategoryTheory.Functor.preservesKernelsOfMapExact {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) (h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.toPrefunctor.map f) (L.toPrefunctor.map g)) (X : A) (Y : A) (f : X ⟶ Y) :

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

A functor which preserves exactness preserves kernels.

Equations

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

Instances For

source

def CategoryTheory.Functor.preservesCokernelsOfMapExact {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) (h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.toPrefunctor.map f) (L.toPrefunctor.map g)) (X : A) (Y : A) (f : X ⟶ Y) :

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

A functor which preserves exactness preserves zero cokernels.

Equations

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

Instances For

source

def CategoryTheory.Functor.preservesFiniteLimitsOfMapExact {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) (h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.toPrefunctor.map f) (L.toPrefunctor.map g)) :

CategoryTheory.Limits.PreservesFiniteLimits L

A functor which preserves exactness is left exact, i.e. preserves finite limits. This is part of the inverse implication to Functor.map_exact.

Equations

CategoryTheory.Functor.preservesFiniteLimitsOfMapExact L h = CategoryTheory.Functor.preservesFiniteLimitsOfPreservesKernels L

Instances For

source

def CategoryTheory.Functor.preservesFiniteColimitsOfMapExact {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) (h : ∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.toPrefunctor.map f) (L.toPrefunctor.map g)) :

CategoryTheory.Limits.PreservesFiniteColimits L

A functor which preserves exactness is right exact, i.e. preserves finite colimits. This is part of the inverse implication to Functor.map_exact.

Equations

CategoryTheory.Functor.preservesFiniteColimitsOfMapExact L h = CategoryTheory.Functor.preservesFiniteColimitsOfPreservesCokernels L

Instances For

source

def CategoryTheory.Functor.preservesFiniteLimitsOfPreservesMonosAndCokernels {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) [CategoryTheory.Functor.PreservesZeroMorphisms L] [CategoryTheory.Functor.PreservesMonomorphisms L] [{X Y : A} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) L] :

CategoryTheory.Limits.PreservesFiniteLimits L

A functor preserving zero morphisms, monos, and cokernels preserves finite limits.

Equations

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

Instances For

source

def CategoryTheory.Functor.preservesFiniteColimitsOfPreservesEpisAndKernels {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) [CategoryTheory.Functor.PreservesZeroMorphisms L] [CategoryTheory.Functor.PreservesEpimorphisms L] [{X Y : A} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) L] :

CategoryTheory.Limits.PreservesFiniteColimits L

A functor preserving zero morphisms, epis, and kernels preserves finite colimits.

Equations

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

Instances For

Documentation

Mathlib.CategoryTheory.Abelian.Exact

Exact sequences in abelian categories #

Main results #