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
.
The category of finite types.
Equations
Construct a bundled Fintype
from the underlying type and typeclass.
Equations
Equations
- Fintype.inhabited = {default := {α := pempty, str := fintype.of_is_empty pempty.is_empty}}
Equations
The fully faithful embedding of Fintype
into the category of types.
Instances for Fintype.incl
Equivalences between finite types are the same as isomorphisms in Fintype
.
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
- Fintype.skeleton.mk = ulift.up
Equations
Given any object of Fintype.skeleton
, this returns the associated natural number.
Equations
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}
The canonical fully faithful embedding of Fintype.skeleton
into Fintype
.
Equations
- Fintype.skeleton.incl = {obj := λ (X : Fintype.skeleton), Fintype.of (ulift (fin X.len)), map := λ (_x _x_1 : Fintype.skeleton) (f : _x ⟶ _x_1), f, map_id' := Fintype.skeleton.incl._proof_1, map_comp' := Fintype.skeleton.incl._proof_2}
Equations
- Fintype.skeleton.incl.category_theory.full = {preimage := λ (_x _x_1 : Fintype.skeleton) (f : Fintype.skeleton.incl.obj _x ⟶ Fintype.skeleton.incl.obj _x_1), f, witness' := Fintype.skeleton.incl.category_theory.full._proof_1}
The equivalence between Fintype.skeleton
and Fintype
.
Fintype.skeleton
is a skeleton of Fintype
.