Creation of finite limits

This file defines the classes CreatesFiniteLimits, CreatesFiniteColimits, CreatesFiniteProducts and CreatesFiniteCoproducts.

class CategoryTheory.Limits.CreatesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

We say that a functor creates finite limits if it creates all limits of shape J where J : Type is a finite category.

• createsFiniteLimits (J : Type) [SmallCategory J] [FinCategory J] : CreatesLimitsOfShape J F

  F creates all finite limits.

@[implicit_reducible, instance 100]

noncomputable instance CategoryTheory.Limits.createsLimitsOfShapeOfCreatesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteLimits F] (J : Type w) [SmallCategory J] [FinCategory J] : CreatesLimitsOfShape J F

Equations

• CategoryTheory.Limits.createsLimitsOfShapeOfCreatesFiniteLimits F J = CategoryTheory.createsLimitsOfShapeOfEquiv (CategoryTheory.FinCategory.equivAsType J) F

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.CreatesLimitsOfSize.createsFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesFiniteLimits F

If F creates limits of any size, it creates finite limits.

Equations

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

@[implicit_reducible, instance 120]

noncomputable instance CategoryTheory.Limits.CreatesLimitsOfSize0.createsFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] : CreatesFiniteLimits F

Equations

• CategoryTheory.Limits.CreatesLimitsOfSize0.createsFiniteLimits F = CategoryTheory.Limits.CreatesLimitsOfSize.createsFiniteLimits F

@[implicit_reducible, instance 100]

noncomputable instance CategoryTheory.Limits.CreatesLimits.createsFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesLimits F] : CreatesFiniteLimits F

Equations

• CategoryTheory.Limits.CreatesLimits.createsFiniteLimits F = CategoryTheory.Limits.CreatesLimitsOfSize.createsFiniteLimits F

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsOfCreatesFiniteLimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (h : (J : Type w) → {x : SmallCategory J} → FinCategory J → CreatesLimitsOfShape J F) : CreatesFiniteLimits F

If F creates finite limits in any universe, then it creates finite limits.

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.compCreatesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesFiniteLimits F] [CreatesFiniteLimits G] : CreatesFiniteLimits (F.comp G)

Equations

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

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteLimitsOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {h : F ≅ G} [CreatesFiniteLimits F] : CreatesFiniteLimits G

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

Equations

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

theorem CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [HasFiniteLimits D] [CreatesFiniteLimits F] : HasFiniteLimits C

@[instance 100]

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

class CategoryTheory.Limits.CreatesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

We say that a functor creates finite products if it creates all limits of shape Discrete J where J : Type is finite.

• creates (J : Type) [Fintype J] : CreatesLimitsOfShape (Discrete J) F

  F creates all finite limits.

@[implicit_reducible]

def CategoryTheory.Limits.CreatesFiniteProducts.mk' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (H : (J : Type w) → [Fintype J] → CreatesLimitsOfShape (Discrete J) F) : CreatesFiniteProducts F

The condition of CreatesFiniteProducts can be checked for finite types in an arbitrary universe.

Equations

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

@[implicit_reducible, instance 100]

noncomputable instance CategoryTheory.Limits.createsLimitsOfShapeOfCreatesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteProducts F] (J : Type w) [Finite J] : CreatesLimitsOfShape (Discrete J) F

Equations

• CategoryTheory.Limits.createsLimitsOfShapeOfCreatesFiniteProducts F J = CategoryTheory.createsLimitsOfShapeOfEquiv (CategoryTheory.Discrete.equivalence ⋯.some.symm) F

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.compCreatesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesFiniteProducts F] [CreatesFiniteProducts G] : CreatesFiniteProducts (F.comp G)

Equations

• CategoryTheory.Limits.compCreatesFiniteProducts F G = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.compCreatesLimitsOfShape F G }

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteProductsOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {h : F ≅ G} [CreatesFiniteProducts F] : CreatesFiniteProducts G

Transfer creation of finite products along a natural isomorphism in the functor.

Equations

• CategoryTheory.Limits.createsFiniteProductsOfNatIso = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.createsLimitsOfShapeOfNatIso h }

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.instCreatesFiniteProductsOfCreatesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteLimits F] : CreatesFiniteProducts F

Equations

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

class CategoryTheory.Limits.CreatesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

We say that a functor creates finite colimits if it creates all colimits of shape J where J : Type is a finite category.

• createsFiniteColimits (J : Type) [SmallCategory J] [FinCategory J] : CreatesColimitsOfShape J F

  F creates all finite colimits.

@[implicit_reducible, instance 100]

noncomputable instance CategoryTheory.Limits.createsColimitsOfShapeOfCreatesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteColimits F] (J : Type w) [SmallCategory J] [FinCategory J] : CreatesColimitsOfShape J F

Equations

• CategoryTheory.Limits.createsColimitsOfShapeOfCreatesFiniteColimits F J = CategoryTheory.createsColimitsOfShapeOfEquiv (CategoryTheory.FinCategory.equivAsType J) F

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.CreatesColimitsOfSize.createsFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CreatesFiniteColimits F

If F creates colimits of any size, it creates finite colimits.

Equations

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

@[implicit_reducible, instance 120]

noncomputable instance CategoryTheory.Limits.CreatesColimitsOfSize0.createsFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] : CreatesFiniteColimits F

Equations

• CategoryTheory.Limits.CreatesColimitsOfSize0.createsFiniteColimits F = CategoryTheory.Limits.CreatesColimitsOfSize.createsFiniteColimits F

@[implicit_reducible, instance 100]

noncomputable instance CategoryTheory.Limits.CreatesColimits.createsFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesColimits F] : CreatesFiniteColimits F

Equations

• CategoryTheory.Limits.CreatesColimits.createsFiniteColimits F = CategoryTheory.Limits.CreatesColimitsOfSize.createsFiniteColimits F

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsOfCreatesFiniteColimitsOfSize {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (h : (J : Type w) → {x : SmallCategory J} → FinCategory J → CreatesColimitsOfShape J F) : CreatesFiniteColimits F

If F creates finite colimits in any universe, then it creates finite colimits.

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.compCreatesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesFiniteColimits F] [CreatesFiniteColimits G] : CreatesFiniteColimits (F.comp G)

Equations

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

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteColimitsOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {h : F ≅ G} [CreatesFiniteColimits F] : CreatesFiniteColimits G

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

Equations

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

theorem CategoryTheory.Limits.hasFiniteColimits_of_hasColimits_of_createsFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [HasFiniteColimits D] [CreatesFiniteColimits F] : HasFiniteColimits C

@[instance 100]

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

class CategoryTheory.Limits.CreatesFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max (max (max 1 u₁) u₂) v₁) v₂)

We say that a functor creates finite limits if it creates all limits of shape J where J : Type is a finite category.

• creates (J : Type) [Fintype J] : CreatesColimitsOfShape (Discrete J) F

  F creates all finite limits.

@[implicit_reducible, instance 100]

noncomputable instance CategoryTheory.Limits.createsColimitsOfShapeOfCreatesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteCoproducts F] (J : Type w) [Finite J] : CreatesColimitsOfShape (Discrete J) F

Equations

• CategoryTheory.Limits.createsColimitsOfShapeOfCreatesFiniteProducts F J = CategoryTheory.createsColimitsOfShapeOfEquiv (CategoryTheory.Discrete.equivalence ⋯.some.symm) F

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.compCreatesFiniteCoproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [CreatesFiniteCoproducts F] [CreatesFiniteCoproducts G] : CreatesFiniteCoproducts (F.comp G)

Equations

• CategoryTheory.Limits.compCreatesFiniteCoproducts F G = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.compCreatesColimitsOfShape F G }

@[implicit_reducible]

def CategoryTheory.Limits.createsFiniteCoproductsOfNatIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {h : F ≅ G} [CreatesFiniteCoproducts F] : CreatesFiniteCoproducts G

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

Equations

• CategoryTheory.Limits.createsFiniteCoproductsOfNatIso = { creates := fun (x : Type) (x_1 : Fintype x) => CategoryTheory.createsColimitsOfShapeOfNatIso h }

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.instCreatesFiniteCoproductsOfCreatesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [CreatesFiniteColimits F] : CreatesFiniteCoproducts F

Equations

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