# 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
@[instance]
def Fintype.of (X : Type u_1) [fintype X] :

Construct a bundled Fintype from the underlying type and typeclass.

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

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

Equations
@[simp]
theorem Fintype.incl_obj  :
= c.α
@[instance]
Equations
def Fintype.skeleton  :
Type

The "standard" skeleton for Fintype. This is the full subcategory of Fintype spanned by objects of the form fin n for n : ℕ. We parameterize the objects of Fintype.skeleton directly as ℕ, as the type fin m ≃ fin n is nonempty if and only if n = m.

Equations

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

Equations
@[instance]
Equations

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

Equations
@[instance]
Equations

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

Equations
@[instance]
Equations
@[instance]
Equations

The equivalence between Fintype.skeleton and Fintype.

Equations
@[simp]

Fintype.skeleton is a skeleton of Fintype.

Equations