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

@[instance 100]

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.

@[instance 120]

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

@[instance 120]

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.

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 (F.comp G)

The composition of two left exact functors is left exact.

Equations

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

def CategoryTheory.Limits.preservesFiniteLimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteLimits G

Transfer preservation of finite limits along a natural isomorphism in the functor.

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 100]

noncomputable instance CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (J : Type u) [Finite J] [CategoryTheory.Limits.PreservesFiniteProducts F] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F

Equations

• CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts F J = ⋯.some

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 (F.comp G)

Equations

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

noncomputable instance CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits {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.instPreservesFiniteProductsOfPreservesFiniteLimits F = { preserves := fun (x : Type) (x_1 : Fintype x) => inferInstance }

class CategoryTheory.Limits.ReflectsFiniteLimits {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 reflect finite limits, if it reflects all limits of shape J, where J : Type is a finite category.

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

class CategoryTheory.Limits.ReflectsFiniteProducts {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 reflects limits of shape Discrete J for finite J

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

noncomputable def CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsFiniteLimits F

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

Equations

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

@[instance 120]

noncomputable instance CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsFiniteLimits F

Equations

• CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimitsOfSize F = CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits F

@[instance 120]

noncomputable instance CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimits F] : CategoryTheory.Limits.ReflectsFiniteLimits F

Equations

• CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits F = CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsFiniteLimits F

def CategoryTheory.Limits.preservesFiniteLimitsOfReflectsOfPreserves {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.comp G)] [CategoryTheory.Limits.ReflectsFiniteLimits G] : CategoryTheory.Limits.PreservesFiniteLimits F

If F ⋙ G preserves finite limits and G reflects finite limits, then F preserves finite limits.

Equations

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

def CategoryTheory.Limits.preservesFiniteProductsOfReflectsOfPreserves {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.comp G)] [CategoryTheory.Limits.ReflectsFiniteProducts G] : CategoryTheory.Limits.PreservesFiniteProducts F

If F ⋙ G preserves finite products and G reflects finite products, then F preserves finite products.

Equations

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

noncomputable instance CategoryTheory.Limits.reflectsFiniteLimitsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.ReflectsFiniteLimits F

Equations

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

noncomputable instance CategoryTheory.Limits.reflectsFiniteProductsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.PreservesFiniteProducts F] : CategoryTheory.Limits.ReflectsFiniteProducts F

Equations

• CategoryTheory.Limits.reflectsFiniteProductsOfReflectsIsomorphisms F = { reflects := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms }

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

Equations

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

noncomputable instance CategoryTheory.Limits.instReflectsFiniteProductsOfReflectsFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteLimits F] : CategoryTheory.Limits.ReflectsFiniteProducts F

Equations

• CategoryTheory.Limits.instReflectsFiniteProductsOfReflectsFiniteLimits F = { reflects := 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

@[instance 100]

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 colimits also implies preserving colimits 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.

@[instance 120]

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

@[instance 120]

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.

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 (F.comp G)

The composition of two right exact functors is right exact.

Equations

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

def CategoryTheory.Limits.preservesFiniteColimitsOfNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteColimits G

Transfer preservation of finite colimits along a natural isomorphism in the functor.

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

  preservation of colimits indexed by Discrete J when [Fintype J]

@[instance 100]

noncomputable instance CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (J : Type u) [Finite J] [CategoryTheory.Limits.PreservesFiniteCoproducts F] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F

Equations

• CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts F J = ⋯.some

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 (F.comp G)

Equations

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

noncomputable instance CategoryTheory.Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits {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.instPreservesFiniteCoproductsOfPreservesFiniteColimits F = { preserves := fun (x : Type) (x_1 : Fintype x) => inferInstance }

class CategoryTheory.Limits.ReflectsFiniteColimits {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 reflect finite colimits, if it reflects all colimits of shape J, where J : Type is a finite category.

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

noncomputable def CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsFiniteColimits F

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

Equations

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

@[instance 120]

noncomputable instance CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.ReflectsFiniteColimits F

Equations

• CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimitsOfSize F = CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits F

@[instance 120]

noncomputable instance CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimits F] : CategoryTheory.Limits.ReflectsFiniteColimits F

Equations

• CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits F = CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsFiniteColimits F

class CategoryTheory.Limits.ReflectsFiniteCoproducts {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 coproducts if it reflects colimits of shape Discrete J for finite J

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

def CategoryTheory.Limits.preservesFiniteColimitsOfReflectsOfPreserves {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.comp G)] [CategoryTheory.Limits.ReflectsFiniteColimits G] : CategoryTheory.Limits.PreservesFiniteColimits F

If F ⋙ G preserves finite colimits and G reflects finite colimits, then F preserves finite colimits.

Equations

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

noncomputable def CategoryTheory.Limits.preservesFiniteCoproductsOfReflectsOfPreserves {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.comp G)] [CategoryTheory.Limits.ReflectsFiniteCoproducts G] : CategoryTheory.Limits.PreservesFiniteCoproducts F

If F ⋙ G preserves finite coproducts and G reflects finite coproducts, then F preserves finite coproducts.

Equations

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

noncomputable instance CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.ReflectsFiniteColimits F

Equations

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

noncomputable instance CategoryTheory.Limits.reflectsFiniteCoproductsOfReflectsIsomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.PreservesFiniteCoproducts F] : CategoryTheory.Limits.ReflectsFiniteCoproducts F

Equations

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

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

Equations

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

noncomputable instance CategoryTheory.Limits.instReflectsFiniteCoproductsOfReflectsFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsFiniteColimits F] : CategoryTheory.Limits.ReflectsFiniteCoproducts F

Equations

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