Documentation

Mathlib.CategoryTheory.Limits.FintypeCat

(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.

noncomputable instance CategoryTheory.Limits.FintypeCat.finiteLimitOfFiniteDiagram {J : Type} [SmallCategory J] [FinCategory J] (K : 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
Equations
  • One or more equations did not get rendered due to their size.
noncomputable def CategoryTheory.Limits.FintypeCat.productEquiv {ι : Type u_1} [Finite ι] (X : ιFintypeCat) :
(∏ᶜ X).carrier ((i : ι) → (X i).carrier)

The categorical product of a finite family in FintypeCat is equivalent to the product as types.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Limits.FintypeCat.productEquiv_apply {ι : Type u_1} [Finite ι] (X : ιFintypeCat) (x : (∏ᶜ X).carrier) (i : ι) :
    (productEquiv X) x i = Pi.π X i x
    @[simp]
    theorem CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply {ι : Type u_1} [Finite ι] (X : ιFintypeCat) (x : (i : ι) → (X i).carrier) (i : ι) :
    Pi.π X i ((productEquiv X).symm x) = x i
    noncomputable instance CategoryTheory.Limits.FintypeCat.finiteColimitOfFiniteDiagram {J : Type} [SmallCategory J] [FinCategory J] (K : 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.

    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    theorem CategoryTheory.Limits.FintypeCat.jointly_surjective {J : Type u_1} [Category.{u_1, u_1} J] [FinCategory J] (F : Functor J FintypeCat) (t : Cocone F) (h : IsColimit t) (x : t.pt.carrier) :
    ∃ (j : J) (y : (F.obj j).carrier), t.ι.app j y = x