(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.instFiniteObjCompFintypeCatIncl
{J : Type}
[CategoryTheory.SmallCategory J]
(K : CategoryTheory.Functor J FintypeCat)
(j : J)
:
Finite ((K.comp 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)]
:
Any functor from a finite category to Types that only involves finite objects, has a finite limit.
Equations
noncomputable instance
CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits
{J : Type}
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
CategoryTheory.Limits.FintypeCat.instCreatesLimitsOfShapeFintypeCatForgetOfFinCategory
{J : Type}
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
:
Equations
- CategoryTheory.Limits.FintypeCat.instCreatesLimitsOfShapeFintypeCatForgetOfFinCategory = CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteLimits
Equations
- One or more equations did not get rendered due to their size.
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)]
:
Any functor from a finite category to Types that only involves finite objects, has a finite colimit.
noncomputable instance
CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits
{J : Type}
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
CategoryTheory.Limits.FintypeCat.instCreatesColimitsOfShapeFintypeCatForgetOfFinCategory
{J : Type}
[CategoryTheory.SmallCategory J]
[CategoryTheory.FinCategory J]
:
Equations
- CategoryTheory.Limits.FintypeCat.instCreatesColimitsOfShapeFintypeCatForgetOfFinCategory = CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForget :