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) [F.PreservesZeroMorphisms] {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.

Equations

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

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) [F.PreservesZeroMorphisms] [{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] {X : C} {Y : C} : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) F

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

Equations

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

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) [F.PreservesZeroMorphisms] [{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F

A kernel preserving functor between preadditive categories preserves binary products.

Equations

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

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) [F.PreservesZeroMorphisms] [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) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F

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

Equations

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

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) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair F

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

Equations

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

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) [F.PreservesZeroMorphisms] [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] : CategoryTheory.Limits.PreservesFiniteLimits F

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

Equations

• F.preservesFiniteLimitsOfPreservesKernels = CategoryTheory.Limits.preservesFiniteLimitsOfPreservesEqualizersAndFiniteProducts F

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) [F.PreservesZeroMorphisms] {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.

Equations

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

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) [F.PreservesZeroMorphisms] [{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] {X : C} {Y : C} : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.pair X Y) F

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

Equations

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

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) [F.PreservesZeroMorphisms] [{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F

A cokernel preserving functor between preadditive categories preserves binary coproducts.

Equations

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

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) [F.PreservesZeroMorphisms] [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) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) F

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

Equations

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

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) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [{X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair F

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

Equations

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

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) [F.PreservesZeroMorphisms] [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] : CategoryTheory.Limits.PreservesFiniteColimits F

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

Equations

• F.preservesFiniteColimitsOfPreservesCokernels = CategoryTheory.Limits.preservesFiniteColimitsOfPreservesCoequalizersAndFiniteCoproducts F