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₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y Z : C} (π₁ : Z ⟶ X) (π₂ : Z ⟶ Y) [Limits.PreservesLimit (Limits.parallelPair π₂ 0) F] (i : Limits.IsLimit (Limits.BinaryFan.mk π₁ π₂)) : Limits.IsLimit (F.mapCone (Limits.BinaryFan.mk π₁ π₂))

A functor between preadditive categories which preserves kernels preserves that an arbitrary binary fan is a limit.

theorem CategoryTheory.Functor.preservesBinaryProduct_of_preservesKernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) F] {X Y : C} : Limits.PreservesLimit (Limits.pair X Y) F

A kernel preserving functor between preadditive categories preserves any pair being a limit.

theorem CategoryTheory.Functor.preservesBinaryProducts_of_preservesKernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) F] : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F

A kernel preserving functor between preadditive categories preserves binary products.

theorem CategoryTheory.Functor.preservesEqualizer_of_preservesKernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasBinaryBiproducts C] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) F] {X Y : C} (f g : X ⟶ Y) : Limits.PreservesLimit (Limits.parallelPair f g) F

A functor between preadditive categories preserves the equalizer of two morphisms if it preserves all kernels.

theorem CategoryTheory.Functor.preservesEqualizers_of_preservesKernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasBinaryBiproducts C] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) F] : Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F

A functor between preadditive categories preserves all equalizers if it preserves all kernels.

theorem CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasBinaryBiproducts C] [Limits.HasFiniteProducts C] [Limits.HasEqualizers C] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) F] : Limits.PreservesFiniteLimits F

A functor between preadditive categories which preserves kernels preserves all finite limits.

def CategoryTheory.Functor.isColimitMapCoconeBinaryCofanOfPreservesCokernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y Z : C} (ι₁ : X ⟶ Z) (ι₂ : Y ⟶ Z) [Limits.PreservesColimit (Limits.parallelPair ι₂ 0) F] (i : Limits.IsColimit (Limits.BinaryCofan.mk ι₁ ι₂)) : Limits.IsColimit (F.mapCocone (Limits.BinaryCofan.mk ι₁ ι₂))

A functor between preadditive categories which preserves cokernels preserves finite coproducts.

theorem CategoryTheory.Functor.preservesCoproduct_of_preservesCokernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesColimit (Limits.parallelPair f 0) F] {X Y : C} : Limits.PreservesColimit (Limits.pair X Y) F

A cokernel preserving functor between preadditive categories preserves any pair being a colimit.

theorem CategoryTheory.Functor.preservesBinaryCoproducts_of_preservesCokernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesColimit (Limits.parallelPair f 0) F] : Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) F

A cokernel preserving functor between preadditive categories preserves binary coproducts.

theorem CategoryTheory.Functor.preservesCoequalizer_of_preservesCokernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasBinaryBiproducts C] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesColimit (Limits.parallelPair f 0) F] {X Y : C} (f g : X ⟶ Y) : Limits.PreservesColimit (Limits.parallelPair f g) F

A functor between preadditive categories preserves the coequalizer of two morphisms if it preserves all cokernels.

theorem CategoryTheory.Functor.preservesCoequalizers_of_preservesCokernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasBinaryBiproducts C] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesColimit (Limits.parallelPair f 0) F] : Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F

A functor between preadditive categories preserves all coequalizers if it preserves all kernels.

theorem CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.HasBinaryBiproducts C] [Limits.HasFiniteCoproducts C] [Limits.HasCoequalizers C] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [∀ {X Y : C} (f : X ⟶ Y), Limits.PreservesColimit (Limits.parallelPair f 0) F] : Limits.PreservesFiniteColimits F

A functor between preadditive categories which preserves kernels preserves all finite limits.