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.

source

def Fintype :

Type (u_1+1)

The category of finite types.

Equations

Fintype = category_theory.bundled fintype

Instances for Fintype

source

@[protected, instance]

def Fintype.has_coe_to_sort :

has_coe_to_sort Fintype (Type u_1)

Equations

Fintype.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

source

def Fintype.of (X : Type u_1) [fintype X] :

Fintype

Construct a bundled Fintype from the underlying type and typeclass.

Equations

Fintype.of X = category_theory.bundled.of X

source

@[protected, instance]

def Fintype.inhabited :

inhabited Fintype

Equations

Fintype.inhabited = {default := {α := pempty, str := fintype.of_is_empty pempty.is_empty}}

source

@[protected, instance]

def Fintype.fintype {X : Fintype} :

fintype ↥X

Equations

Fintype.fintype = X.str

source

@[protected, instance]

def Fintype.category_theory.category :

category_theory.category Fintype

Equations

Fintype.category_theory.category = category_theory.induced_category.category category_theory.bundled.α

source

@[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 ᾰ

source

@[protected, instance]

def Fintype.incl.full :

category_theory.full Fintype.incl

source

@[protected, instance]

def Fintype.incl.faithful :

category_theory.faithful Fintype.incl

source

def Fintype.incl :

Fintype ⥤ Type u_1

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

Equations

Fintype.incl = category_theory.induced_functor category_theory.bundled.α

Instances for Fintype.incl

source

@[simp]

theorem Fintype.incl_obj (self : category_theory.bundled fintype) :

Fintype.incl.obj self = self.α

source

@[protected, instance]

def Fintype.concrete_category_Fintype :

category_theory.concrete_category Fintype

Equations

Fintype.concrete_category_Fintype = category_theory.concrete_category.mk Fintype.incl

source

@[simp]

theorem Fintype.id_apply (X : Fintype) (x : ↥X) :

𝟙 X x = x

source

@[simp]

theorem Fintype.comp_apply {X Y Z : Fintype} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) :

(f ≫ g) x = g (f x)

source

@[simp]

theorem Fintype.equiv_equiv_iso_symm_apply_apply {A B : Fintype} (i : A ≅ B) (ᾰ : A.α) :

⇑(⇑(Fintype.equiv_equiv_iso.symm) i) ᾰ = i.hom ᾰ

source

@[simp]

theorem Fintype.equiv_equiv_iso_apply_hom {A B : Fintype} (e : ↥A ≃ ↥B) (ᾰ : ↥A) :

(⇑Fintype.equiv_equiv_iso e).hom ᾰ = ⇑e ᾰ

source

@[simp]

theorem Fintype.equiv_equiv_iso_apply_inv {A B : Fintype} (e : ↥A ≃ ↥B) (ᾰ : ↥B) :

(⇑Fintype.equiv_equiv_iso e).inv ᾰ = ⇑(e.symm) ᾰ

source

def Fintype.equiv_equiv_iso {A B : Fintype} :

↥A ≃ ↥B ≃ (A ≅ B)

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

Equations

Fintype.equiv_equiv_iso = {to_fun := λ (e : ↥A ≃ ↥B), {hom := ⇑e, inv := ⇑(e.symm), hom_inv_id' := _, inv_hom_id' := _}, inv_fun := λ (i : A ≅ B), {to_fun := i.hom, inv_fun := i.inv, left_inv := _, right_inv := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem Fintype.equiv_equiv_iso_symm_apply_symm_apply {A B : Fintype} (i : A ≅ B) (ᾰ : B.α) :

⇑((⇑(Fintype.equiv_equiv_iso.symm) i).symm) ᾰ = i.inv ᾰ

source

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

Fintype.skeleton = ulift ℕ

Instances for Fintype.skeleton

source

def Fintype.skeleton.mk :

ℕ → Fintype.skeleton

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

Equations

Fintype.skeleton.mk = ulift.up

source

@[protected, instance]

def Fintype.skeleton.inhabited :

inhabited Fintype.skeleton

Equations

Fintype.skeleton.inhabited = {default := Fintype.skeleton.mk 0}

source

def Fintype.skeleton.len :

Fintype.skeleton → ℕ

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

Equations

Fintype.skeleton.len = ulift.down

source

@[ext]

theorem Fintype.skeleton.ext (X Y : Fintype.skeleton) :

X.len = Y.len → X = Y

source

@[protected, instance]

def Fintype.skeleton.category_theory.small_category :

category_theory.small_category Fintype.skeleton

Equations

Fintype.skeleton.category_theory.small_category = {to_category_struct := {to_quiver := {hom := λ (X Y : Fintype.skeleton), ulift (fin X.len) → ulift (fin Y.len)}, id := λ (_x : Fintype.skeleton), id, comp := λ (_x _x_1 _x_2 : Fintype.skeleton) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), g ∘ f}, id_comp' := Fintype.skeleton.category_theory.small_category._proof_1, comp_id' := Fintype.skeleton.category_theory.small_category._proof_2, assoc' := Fintype.skeleton.category_theory.small_category._proof_3}