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
.
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.
We can always derive PreservesFiniteLimits C
by showing that we are preserving limits at an
arbitrary universe.
The composition of two left exact functors is left exact.
Transfer preservation of finite limits along a natural isomorphism in the functor.
A functor F
preserves finite products if it preserves all from Discrete J
for Finite J
.
We require this for J = Fin n
in the definition,
then generalize to J : Type u
in the instance.
- preserves (n : Nat) : PreservesLimitsOfShape (Discrete (Fin n)) F
Instances For
A functor F
preserves finite products if it reflects limits of shape Discrete J
for finite J
.
We require this for J = Fin n
in the definition,
then generalize to J : Type u
in the instance.
- reflects (n : Nat) : ReflectsLimitsOfShape (Discrete (Fin n)) F
Instances For
If we reflect limits of some arbitrary size, then we reflect all finite limits.
If F ⋙ G
preserves finite limits and G
reflects finite limits, then F
preserves
finite limits.
If F ⋙ G
preserves finite products and G
reflects finite products, then F
preserves
finite products.
Preserving finite colimits also implies preserving colimits over finite shapes in higher universes.
If we preserve colimits of some arbitrary size, then we preserve all finite colimits.
We can always derive PreservesFiniteColimits C
by showing that we are preserving colimits at an arbitrary universe.
The composition of two right exact functors is right exact.
Transfer preservation of finite colimits along a natural isomorphism in the functor.
A functor F
preserves finite products if it preserves all from Discrete J
for Fintype J
.
We require this for J = Fin n
in the definition,
then generalize to J : Type u
in the instance.
- preserves (n : Nat) : PreservesColimitsOfShape (Discrete (Fin n)) F
preservation of colimits indexed by
Discrete (Fin n)
.
Instances For
If we reflect colimits of some arbitrary size, then we reflect all finite colimits.
A functor F
preserves finite coproducts if it reflects colimits of shape Discrete J
for finite J
.
We require this for J = Fin n
in the definition,
then generalize to J : Type u
in the instance.
- reflects (n : Nat) : ReflectsColimitsOfShape (Discrete (Fin n)) F
Instances For
If F ⋙ G
preserves finite colimits and G
reflects finite colimits, then F
preserves finite
colimits.
If F ⋙ G
preserves finite coproducts and G
reflects finite coproducts, then F
preserves
finite coproducts.