(Co)limits in the category of finite types

We show that finite (co)limits exist in FintypeCat and that they are preserved by the natural inclusion FintypeCat.incl.

instance CategoryTheory.Limits.FintypeCat.instFiniteObjToQuiverToCategoryStructTypeToQuiverToCategoryStructTypesToPrefunctorCompFintypeCatInstCategoryFintypeCatIncl {J : Type} [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J FintypeCat) (j : J) : Finite ((CategoryTheory.Functor.comp K FintypeCat.incl).obj j)

Equations

• ⋯ = ⋯

noncomputable instance CategoryTheory.Limits.FintypeCat.finiteLimitOfFiniteDiagram {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J (Type u_1)) [∀ (j : J), Finite (K.obj j)] : Fintype (CategoryTheory.Limits.limit K)

Any functor from a finite category to Types that only involves finite objects, has a finite limit.

Equations

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

noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.CreatesLimitsOfShape J FintypeCat.incl

Equations

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

noncomputable instance CategoryTheory.Limits.FintypeCat.instCreatesLimitsOfShapeFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget FintypeCat)

Equations

• CategoryTheory.Limits.FintypeCat.instCreatesLimitsOfShapeFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype = CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits

instance CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatInstCategoryFintypeCat {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasLimitsOfShape J FintypeCat

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.FintypeCat.hasFiniteLimits : CategoryTheory.Limits.HasFiniteLimits FintypeCat

Equations

• CategoryTheory.Limits.FintypeCat.hasFiniteLimits = ⋯

noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits FintypeCat.incl

Equations

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

noncomputable instance CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget FintypeCat)

Equations

• CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype = CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteLimits

noncomputable instance CategoryTheory.Limits.FintypeCat.finiteColimitOfFiniteDiagram {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J (Type u_1)) [∀ (j : J), Finite (K.obj j)] : Fintype (CategoryTheory.Limits.colimit K)

Any functor from a finite category to Types that only involves finite objects, has a finite colimit.

Equations

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

noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.CreatesColimitsOfShape J FintypeCat.incl

Equations

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

noncomputable instance CategoryTheory.Limits.FintypeCat.instCreatesColimitsOfShapeFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.forget FintypeCat)

Equations

• CategoryTheory.Limits.FintypeCat.instCreatesColimitsOfShapeFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype = CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits

instance CategoryTheory.Limits.FintypeCat.instHasColimitsOfShapeFintypeCatInstCategoryFintypeCat {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasColimitsOfShape J FintypeCat

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.FintypeCat.hasFiniteColimits : CategoryTheory.Limits.HasFiniteColimits FintypeCat

Equations

• CategoryTheory.Limits.FintypeCat.hasFiniteColimits = ⋯

noncomputable instance CategoryTheory.Limits.FintypeCat.inclusionPreservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits FintypeCat.incl

Equations

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

noncomputable instance CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget FintypeCat)

Equations

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