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 Y 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.
Instances For
theorem
CategoryTheory.Functor.preservesBinaryProduct_of_preservesKernels
{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 Y : C}
:
A kernel preserving functor between preadditive categories preserves any pair being a limit.
theorem
CategoryTheory.Functor.preservesBinaryProducts_of_preservesKernels
{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]
:
A kernel preserving functor between preadditive categories preserves binary products.
theorem
CategoryTheory.Functor.preservesEqualizer_of_preservesKernels
{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 Y : C}
(f g : X ⟶ Y)
:
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₁}
[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]
:
A functor between preadditive categories preserves all equalizers if it preserves all kernels.
theorem
CategoryTheory.Functor.preservesFiniteLimits_of_preservesKernels
{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]
:
A functor between preadditive categories which preserves kernels preserves all finite limits.
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 Y 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.
Instances For
theorem
CategoryTheory.Functor.preservesCoproduct_of_preservesCokernels
{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 Y : C}
:
A cokernel preserving functor between preadditive categories preserves any pair being a colimit.
theorem
CategoryTheory.Functor.preservesBinaryCoproducts_of_preservesCokernels
{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]
:
A cokernel preserving functor between preadditive categories preserves binary coproducts.
theorem
CategoryTheory.Functor.preservesCoequalizer_of_preservesCokernels
{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 Y : C}
(f g : X ⟶ Y)
:
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₁}
[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]
:
A functor between preadditive categories preserves all coequalizers if it preserves all kernels.
theorem
CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels
{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]
:
A functor between preadditive categories which preserves kernels preserves all finite limits.