# mathlibdocumentation

category_theory.Fintype

# The category of finite types. #

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

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

def Fintype  :
Type (u_1+1)

The category of finite types.

Equations
Instances for Fintype
@[protected, instance]
def Fintype.has_coe_to_sort  :
(Type u_1)
Equations
def Fintype.of (X : Type u_1) [fintype X] :

Construct a bundled Fintype from the underlying type and typeclass.

Equations
@[protected, instance]
Equations
@[protected, instance]
def Fintype.fintype {X : Fintype} :
Equations
@[protected, instance]
Equations
@[simp]
theorem Fintype.incl_map (x y : category_theory.induced_category (Type u_1) category_theory.bundled.α) (f : x y) (ᾰ : x.α) :
= f ᾰ
@[protected, instance]
@[protected, instance]
def Fintype.incl  :
Fintype Type u_1

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

Equations
Instances for Fintype.incl
@[simp]
@[protected, instance]
Equations
@[simp]
theorem Fintype.id_apply (X : Fintype) (x : X) :
𝟙 X x = x
@[simp]
theorem Fintype.comp_apply {X Y Z : Fintype} (f : X Y) (g : Y Z) (x : X) :
(f g) x = g (f x)
@[simp]
theorem Fintype.equiv_equiv_iso_symm_apply_apply {A B : Fintype} (i : A B) (ᾰ : A.α) :
= i.hom
@[simp]
theorem Fintype.equiv_equiv_iso_apply_hom {A B : Fintype} (e : A B) (ᾰ : A) :
= e ᾰ
@[simp]
theorem Fintype.equiv_equiv_iso_apply_inv {A B : Fintype} (e : A B) (ᾰ : B) :
= (e.symm) ᾰ
def Fintype.equiv_equiv_iso {A B : Fintype} :
A B (A B)

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

Equations
@[simp]
theorem Fintype.equiv_equiv_iso_symm_apply_symm_apply {A B : Fintype} (i : A B) (ᾰ : B.α) :
def Fintype.skeleton  :
Type u

The "standard" skeleton for Fintype. This is the full subcategory of Fintype 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 Fintype.skeleton

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

Equations
@[protected, instance]
Equations

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

Equations
@[ext]
theorem Fintype.skeleton.ext (X Y : Fintype.skeleton) :
X.len = Y.lenX = Y
@[protected, instance]
Equations

The canonical fully faithful embedding of Fintype.skeleton into Fintype.

Equations
Instances for Fintype.skeleton.incl
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
noncomputable def Fintype.skeleton.equivalence  :

The equivalence between Fintype.skeleton and Fintype.

Equations
@[simp]

Fintype.skeleton is a skeleton of Fintype.

Equations