mathlib documentation

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

Construct a bundled Fintype from the underlying type and typeclass.

Equations
@[instance]

Equations
def Fintype.incl  :
Fintype Type u_1

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

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

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