# mathlib3documentation

category_theory.Fintype

# The category of finite types. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
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 (f : x y) (ᾰ : x.α) :
= f ᾰ
@[protected, instance]
@[protected, instance]

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.α) :

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.len X = 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