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 : see CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean. Also provides the dual version.
• CategoryTheory.Limits.preservesFiniteLimitsIffFlat : see CategoryTheory/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₂)

A functor is said to preserve finite limits, if it preserves all limits of shape J, where J : Type is a finite category.

• preservesFiniteLimits : (J : Type) → [inst : CategoryTheory.SmallCategory J] → [inst_1 : CategoryTheory.FinCategory J] → CategoryTheory.Limits.PreservesLimitsOfShape J F

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] : CategoryTheory.Limits.PreservesLimitsOfShape J F

Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.

Equations

• CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits F J = CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv (CategoryTheory.FinCategory.equivAsType J) F

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

If we preserve limits of some arbitrary size, then we preserve all finite limits.

Equations

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

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

Equations

• CategoryTheory.Limits.PreservesLimitsOfSize0.preservesFiniteLimits F = CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits 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] : CategoryTheory.Limits.PreservesFiniteLimits F

Equations

• CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits F = CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits 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) : CategoryTheory.Limits.PreservesFiniteLimits F

We can always derive PreservesFiniteLimits C by showing that we are preserving limits at an arbitrary universe.

Equations

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

noncomputable instance CategoryTheory.Limits.idPreservesFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Functor.id C)

Equations

• CategoryTheory.Limits.idPreservesFiniteLimits = { preservesFiniteLimits := fun (x : Type) (x_1 : CategoryTheory.SmallCategory x) (x_2 : CategoryTheory.FinCategory x) => inferInstance }

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] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Functor.comp F G)

The composition of two left exact functors is left exact.

Equations

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

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₂)

A functor F preserves finite products if it preserves all from Discrete J for Fintype J

• preserves : (J : Type) → [inst : Fintype J] → CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F

instance CategoryTheory.Limits.compPreservesFiniteProducts {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.PreservesFiniteProducts F] [CategoryTheory.Limits.PreservesFiniteProducts G] : CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.Functor.comp F G)

Equations

• CategoryTheory.Limits.compPreservesFiniteProducts F G = { preserves := fun (x : Type) (x_1 : Fintype x) => inferInstance }

noncomputable instance CategoryTheory.Limits.instPreservesFiniteProducts {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] : CategoryTheory.Limits.PreservesFiniteProducts F

Equations

• CategoryTheory.Limits.instPreservesFiniteProducts F = { preserves := fun (x : Type) (x_1 : Fintype x) => inferInstance }

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₂)

A functor is said to preserve finite colimits, if it preserves all colimits of shape J, where J : Type is a finite category.

• preservesFiniteColimits : (J : Type) → [inst : CategoryTheory.SmallCategory J] → [inst_1 : CategoryTheory.FinCategory J] → CategoryTheory.Limits.PreservesColimitsOfShape J F

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] : CategoryTheory.Limits.PreservesColimitsOfShape J F

Preserving finite limits also implies preserving limits over finite shapes in higher universes, though through a noncomputable instance.

Equations

• CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits F J = CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv (CategoryTheory.FinCategory.equivAsType J) F

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

If we preserve colimits of some arbitrary size, then we preserve all finite colimits.

Equations

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

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

Equations

• CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits F = CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits 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] : CategoryTheory.Limits.PreservesFiniteColimits F

Equations

• CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits F = CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits 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) : CategoryTheory.Limits.PreservesFiniteColimits F

We can always derive PreservesFiniteColimits C by showing that we are preserving colimits at an arbitrary universe.

Equations

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

noncomputable instance CategoryTheory.Limits.idPreservesFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Functor.id C)

Equations

• CategoryTheory.Limits.idPreservesFiniteColimits = CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits (CategoryTheory.Functor.id 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] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Functor.comp F G)

The composition of two right exact functors is right exact.

Equations

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

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₂)

A functor F preserves finite products if it preserves all from Discrete J for Fintype J

• preserves : (J : Type) → [inst : Fintype J] → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F

instance CategoryTheory.Limits.compPreservesFiniteCoproducts {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.PreservesFiniteCoproducts F] [CategoryTheory.Limits.PreservesFiniteCoproducts G] : CategoryTheory.Limits.PreservesFiniteCoproducts (CategoryTheory.Functor.comp F G)

Equations

• CategoryTheory.Limits.compPreservesFiniteCoproducts F G = { preserves := fun (x : Type) (x_1 : Fintype x) => inferInstance }

noncomputable instance CategoryTheory.Limits.instPreservesFiniteCoproducts {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] : CategoryTheory.Limits.PreservesFiniteCoproducts F

Equations

• CategoryTheory.Limits.instPreservesFiniteCoproducts F = { preserves := fun (x : Type) (x_1 : Fintype x) => inferInstance }