mathlib3 documentation

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

Construct a bundled Fintype from the underlying type and typeclass.

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.α) :
Fintype.incl.map f = f ᾰ

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

Equations
Instances for Fintype.incl
@[simp]
@[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.α) :
@[simp]
theorem Fintype.equiv_equiv_iso_apply_hom {A B : Fintype} (e : A B) (ᾰ : A) :
@[simp]
theorem Fintype.equiv_equiv_iso_apply_inv {A B : Fintype} (e : A B) (ᾰ : B) :
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

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