Preservation of finite (co)limits. #
These functors are also known as left exact (flat) or right exact functors when the categories involved are abelian, or more generally, finitely (co)complete.
Related results #
CategoryTheory.Limits.preservesFiniteLimitsOfPreservesEqualizersAndFiniteProducts
: seeCategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
. Also provides the dual version.CategoryTheory.Limits.preservesFiniteLimitsIffFlat
: seeCategoryTheory/Functor/Flat.lean
.
- preservesFiniteLimits : (J : Type) → [inst : CategoryTheory.SmallCategory J] → [inst_1 : CategoryTheory.FinCategory J] → CategoryTheory.Limits.PreservesLimitsOfShape J F
A functor is said to preserve finite limits, if it preserves all limits of shape J
,
where J : Type
is a finite category.
Instances
Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.
If we preserve limits of some arbitrary size, then we preserve all finite limits.
Instances For
We can always derive PreservesFiniteLimits C
by showing that we are preserving limits at an
arbitrary universe.
Instances For
The composition of two left exact functors is left exact.
Instances For
- preserves : (J : Type) → [inst : Fintype J] → CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F
A functor F
preserves finite products if it preserves all from Discrete J
for Fintype J
Instances
- preservesFiniteColimits : (J : Type) → [inst : CategoryTheory.SmallCategory J] → [inst_1 : CategoryTheory.FinCategory J] → CategoryTheory.Limits.PreservesColimitsOfShape J F
A functor is said to preserve finite colimits, if it preserves all colimits of
shape J
, where J : Type
is a finite category.
Instances
Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.
If we preserve colimits of some arbitrary size, then we preserve all finite colimits.
Instances For
We can always derive PreservesFiniteColimits C
by showing that we are preserving colimits at an arbitrary universe.
Instances For
The composition of two right exact functors is right exact.
Instances For
- preserves : (J : Type) → [inst : Fintype J] → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
A functor F
preserves finite products if it preserves all from Discrete J
for Fintype J