Left exactness of functors between preadditive categories #
We show that a functor is left exact in the sense that it preserves finite limits, if it preserves kernels. The dual result holds for right exact functors and cokernels.
Main results #
- We first derive preservation of binary product in the lemma
preservesBinaryProductsOfPreservesKernels, - then show the preservation of equalizers in
preservesEqualizerOfPreservesKernels, - and then derive the preservation of all finite limits with the usual construction.
def
CategoryTheory.Functor.isLimitMapConeBinaryFanOfPreservesKernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{X : C}
{Y : C}
{Z : C}
(π₁ : Z ⟶ X)
(π₂ : Z ⟶ Y)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair π₂ 0) F]
(i : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk π₁ π₂))
:
CategoryTheory.Limits.IsLimit (F.mapCone (CategoryTheory.Limits.BinaryFan.mk π₁ π₂))
A functor between preadditive categories which preserves kernels preserves that an arbitrary binary fan is a limit.
Instances For
def
CategoryTheory.Functor.preservesBinaryProductOfPreservesKernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
{X : C}
{Y : C}
:
A kernel preserving functor between preadditive categories preserves any pair being a limit.
Instances For
def
CategoryTheory.Functor.preservesBinaryProductsOfPreservesKernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
:
A kernel preserving functor between preadditive categories preserves binary products.
Instances For
def
CategoryTheory.Functor.preservesEqualizerOfPreservesKernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
A functor between preadditive categories preserves the equalizer of two morphisms if it preserves all kernels.
Instances For
def
CategoryTheory.Functor.preservesEqualizersOfPreservesKernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
:
A functor between preadditive categories preserves all equalizers if it preserves all kernels.
Instances For
def
CategoryTheory.Functor.preservesFiniteLimitsOfPreservesKernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasFiniteProducts C]
[CategoryTheory.Limits.HasEqualizers C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
:
A functor between preadditive categories which preserves kernels preserves all finite limits.
Instances For
def
CategoryTheory.Functor.isColimitMapCoconeBinaryCofanOfPreservesCokernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{X : C}
{Y : C}
{Z : C}
(ι₁ : X ⟶ Z)
(ι₂ : Y ⟶ Z)
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair ι₂ 0) F]
(i : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂))
:
CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂))
A functor between preadditive categories which preserves cokernels preserves finite coproducts.
Instances For
def
CategoryTheory.Functor.preservesCoproductOfPreservesCokernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
{X : C}
{Y : C}
:
A cokernel preserving functor between preadditive categories preserves any pair being a colimit.
Instances For
def
CategoryTheory.Functor.preservesBinaryCoproductsOfPreservesCokernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
:
A cokernel preserving functor between preadditive categories preserves binary coproducts.
Instances For
def
CategoryTheory.Functor.preservesCoequalizerOfPreservesCokernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
A functor between preadditive categories preserves the coequalizer of two morphisms if it preserves all cokernels.
Instances For
def
CategoryTheory.Functor.preservesCoequalizersOfPreservesCokernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
:
A functor between preadditive categories preserves all coequalizers if it preserves all kernels.
Instances For
def
CategoryTheory.Functor.preservesFiniteColimitsOfPreservesCokernels
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
[CategoryTheory.Limits.HasCoequalizers C]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
:
A functor between preadditive categories which preserves kernels preserves all finite limits.