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.
class
CategoryTheory.Limits.PreservesFiniteLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max 1 u₁) u₂) v₁) v₂)
- 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
noncomputable instance
CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesFiniteLimits F]
(J : Type w)
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
:
Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.
noncomputable def
CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F]
:
If we preserve limits of some arbitrary size, then we preserve all finite limits.
Instances For
noncomputable instance
CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F]
:
noncomputable instance
CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimits F]
:
def
CategoryTheory.Limits.preservesFiniteLimitsOfPreservesFiniteLimitsOfSize
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
(h : (J : Type w) →
{𝒥 : CategoryTheory.SmallCategory J} → CategoryTheory.FinCategory J → CategoryTheory.Limits.PreservesLimitsOfShape J F)
:
We can always derive PreservesFiniteLimits C by showing that we are preserving limits at an
arbitrary universe.
Instances For
noncomputable instance
CategoryTheory.Limits.idPreservesFiniteLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
def
CategoryTheory.Limits.compPreservesFiniteLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesFiniteLimits F]
[CategoryTheory.Limits.PreservesFiniteLimits G]
:
The composition of two left exact functors is left exact.
Instances For
class
CategoryTheory.Limits.PreservesFiniteProducts
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max 1 u₁) u₂) v₁) v₂)
- 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
class
CategoryTheory.Limits.PreservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max 1 u₁) u₂) v₁) v₂)
- 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
noncomputable instance
CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesFiniteColimits F]
(J : Type w)
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
:
Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.
noncomputable def
CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F]
:
If we preserve colimits of some arbitrary size, then we preserve all finite colimits.
Instances For
noncomputable instance
CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F]
:
noncomputable instance
CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesColimits F]
:
def
CategoryTheory.Limits.preservesFiniteColimitsOfPreservesFiniteColimitsOfSize
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
(h : (J : Type w) →
{𝒥 : CategoryTheory.SmallCategory J} →
CategoryTheory.FinCategory J → CategoryTheory.Limits.PreservesColimitsOfShape J F)
:
We can always derive PreservesFiniteColimits C
by showing that we are preserving colimits at an arbitrary universe.
Instances For
noncomputable instance
CategoryTheory.Limits.idPreservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
def
CategoryTheory.Limits.compPreservesFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesFiniteColimits F]
[CategoryTheory.Limits.PreservesFiniteColimits G]
:
The composition of two right exact functors is right exact.
Instances For
class
CategoryTheory.Limits.PreservesFiniteCoproducts
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max 1 u₁) u₂) v₁) v₂)
- 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