# The category of finite types. #

We define the category of finite types, denoted FintypeCat as (bundled) types with a Fintype instance.

We also define FintypeCat.Skeleton, the standard skeleton of FintypeCat whose objects are Fin n for n : ℕ. We prove that the obvious inclusion functor FintypeCat.Skeleton ⥤ FintypeCat is an equivalence of categories in FintypeCat.Skeleton.equivalence. We prove that FintypeCat.Skeleton is a skeleton of FintypeCat in FintypeCat.isSkeleton.

def FintypeCat :
Type (u_1 + 1)

The category of finite types.

Equations
Instances For
Equations
def FintypeCat.of (X : Type u_1) [] :

Construct a bundled FintypeCat from the underlying type and typeclass.

Equations
Instances For
Equations
Equations
• FintypeCat.instFintypeα = X.str
@[simp]
theorem FintypeCat.incl_map :
∀ {X Y : CategoryTheory.InducedCategory (Type u_1) CategoryTheory.Bundled.α} (f : X Y) (a : X), FintypeCat.incl.map f a = f a
@[simp]
theorem FintypeCat.incl_obj (self : ) :
FintypeCat.incl.obj self = self

The fully faithful embedding of FintypeCat into the category of types.

Equations
Instances For
Equations
@[simp]
theorem FintypeCat.id_apply (X : FintypeCat) (x : X) :
@[simp]
theorem FintypeCat.comp_apply {X : FintypeCat} {Y : FintypeCat} {Z : FintypeCat} (f : X Y) (g : Y Z) (x : X) :
= g (f x)
@[simp]
theorem FintypeCat.hom_inv_id_apply {X : FintypeCat} {Y : FintypeCat} (f : X Y) (x : X) :
f.inv (f.hom x) = x
@[simp]
theorem FintypeCat.inv_hom_id_apply {X : FintypeCat} {Y : FintypeCat} (f : X Y) (y : Y) :
f.hom (f.inv y) = y
theorem FintypeCat.hom_ext_iff {X : FintypeCat} {Y : FintypeCat} {f : X Y} {g : X Y} :
f = g ∀ (x : X), f x = g x
theorem FintypeCat.hom_ext {X : FintypeCat} {Y : FintypeCat} (f : X Y) (g : X Y) (h : ∀ (x : X), f x = g x) :
f = g
@[simp]
theorem FintypeCat.equivEquivIso_symm_apply_apply {A : FintypeCat} {B : FintypeCat} (i : A B) :
∀ (a : A), (FintypeCat.equivEquivIso.symm i) a = i.hom a
@[simp]
theorem FintypeCat.equivEquivIso_symm_apply_symm_apply {A : FintypeCat} {B : FintypeCat} (i : A B) :
∀ (a : B), (FintypeCat.equivEquivIso.symm i).symm a = i.inv a
@[simp]
theorem FintypeCat.equivEquivIso_apply_hom {A : FintypeCat} {B : FintypeCat} (e : A B) (a : A) :
(FintypeCat.equivEquivIso e).hom a = e a
@[simp]
theorem FintypeCat.equivEquivIso_apply_inv {A : FintypeCat} {B : FintypeCat} (e : A B) (a : B) :
(FintypeCat.equivEquivIso e).inv a = e.symm a
def FintypeCat.equivEquivIso {A : FintypeCat} {B : FintypeCat} :
A B (A B)

Equivalences between finite types are the same as isomorphisms in FintypeCat.

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

The "standard" skeleton for FintypeCat. This is the full subcategory of FintypeCat spanned by objects of the form ULift (Fin n) for n : ℕ. We parameterize the objects of Fintype.Skeleton directly as ULift ℕ, as the type ULift (Fin m) ≃ ULift (Fin n) is nonempty if and only if n = m. Specifying universes, Skeleton : Type u is a small skeletal category equivalent to Fintype.{u}.

Equations
Instances For

Given any natural number n, this creates the associated object of Fintype.Skeleton.

Equations
Instances For

Given any object of Fintype.Skeleton, this returns the associated natural number.

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

The canonical fully faithful embedding of Fintype.Skeleton into FintypeCat.

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

The equivalence between Fintype.Skeleton and Fintype.

Equations
Instances For

Fintype.Skeleton is a skeleton of Fintype.