# Documentation

Mathlib.CategoryTheory.FintypeCat

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

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

Construct a bundled FintypeCat from the underlying type and typeclass.

Instances For
@[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.

Instances For
@[simp]
theorem FintypeCat.id_apply (X : FintypeCat) (x : X) :
CategoryTheory.CategoryStruct.id FintypeCat CategoryTheory.Category.toCategoryStruct X x = x
@[simp]
theorem FintypeCat.comp_apply {X : FintypeCat} {Y : FintypeCat} {Z : FintypeCat} (f : X Y) (g : Y Z) (x : X) :
CategoryTheory.CategoryStruct.comp FintypeCat CategoryTheory.Category.toCategoryStruct X Y Z f g x = g (f 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 =
@[simp]
theorem FintypeCat.equivEquivIso_apply_inv {A : FintypeCat} {B : FintypeCat} (e : A B) (a : B) :
FintypeCat.inv FintypeCat.instCategoryFintypeCat A B (FintypeCat.equivEquivIso e) a = e.symm a
@[simp]
theorem FintypeCat.equivEquivIso_apply_hom {A : FintypeCat} {B : FintypeCat} (e : A B) (a : A) :
FintypeCat.hom FintypeCat.instCategoryFintypeCat A B (FintypeCat.equivEquivIso e) a = e a
@[simp]
theorem FintypeCat.equivEquivIso_symm_apply_symm_apply {A : FintypeCat} {B : FintypeCat} (i : A B) :
∀ (a : B), (FintypeCat.equivEquivIso.symm i).symm a =
def FintypeCat.equivEquivIso {A : FintypeCat} {B : FintypeCat} :
A B (A B)

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

The equivalence between Fintype.Skeleton and Fintype.

Instances For

Fintype.Skeleton is a skeleton of Fintype.

Instances For