The category of finite types. #

We define the category of finite types, denoted FintypeCat as (bundled) types with a Fintype instance.

We also define FintypeCat.Skeleton, the standard skeleton of FintypeCat whose objects are Fin n for n : ℕ. We prove that the obvious inclusion functor FintypeCat.Skeleton ⥤ FintypeCat is an equivalence of categories in FintypeCat.Skeleton.equivalence. We prove that FintypeCat.Skeleton is a skeleton of FintypeCat in FintypeCat.isSkeleton.

source

def FintypeCat :

Type (u_1 + 1)

The category of finite types.

Instances For

source

instance FintypeCat.instCoeSortFintypeCatType :

CoeSort FintypeCat (Type u_1)

source

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

FintypeCat

Construct a bundled FintypeCat from the underlying type and typeclass.

Instances For

source

instance FintypeCat.instInhabitedFintypeCat :

Inhabited FintypeCat

source

instance FintypeCat.instFintypeα {X : FintypeCat} :

Fintype ↑X

source

instance FintypeCat.instCategoryFintypeCat :

CategoryTheory.Category.{u_1, u_1 + 1} FintypeCat

source

@[simp]

theorem FintypeCat.incl_map :

∀ {X Y : CategoryTheory.InducedCategory (Type u_1) CategoryTheory.Bundled.α} (f : X ⟶ Y) (a : ↑X), FintypeCat.incl.map f a = f a

source

@[simp]

theorem FintypeCat.incl_obj (self : CategoryTheory.Bundled Fintype) :

FintypeCat.incl.obj self = ↑self

source

def FintypeCat.incl :

CategoryTheory.Functor FintypeCat (Type u_1)

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

Instances For

source

instance FintypeCat.instFullFintypeCatInstCategoryFintypeCatTypeTypesIncl :

CategoryTheory.Full FintypeCat.incl

source

instance FintypeCat.instFaithfulFintypeCatInstCategoryFintypeCatTypeTypesIncl :

CategoryTheory.Faithful FintypeCat.incl

source

instance FintypeCat.concreteCategoryFintype :

CategoryTheory.ConcreteCategory FintypeCat

source

@[simp]

theorem FintypeCat.id_apply (X : FintypeCat) (x : ↑X) :

CategoryTheory.CategoryStruct.id FintypeCat CategoryTheory.Category.toCategoryStruct X x = x

source

@[simp]

theorem FintypeCat.comp_apply {X : FintypeCat} {Y : FintypeCat} {Z : FintypeCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) :

CategoryTheory.CategoryStruct.comp FintypeCat CategoryTheory.Category.toCategoryStruct X Y Z f g x = g (f x)

source

theorem FintypeCat.hom_ext {X : FintypeCat} {Y : FintypeCat} (f : X ⟶ Y) (g : X ⟶ Y) (h : ∀ (x : ↑X), f x = g x) :

f = g

source

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_apply {A : FintypeCat} {B : FintypeCat} (i : A ≅ B) :

∀ (a : ↑A), ↑(↑FintypeCat.equivEquivIso.symm i) a = FintypeCat.hom FintypeCat.instCategoryFintypeCat A B i a

source

@[simp]

theorem FintypeCat.equivEquivIso_apply_inv {A : FintypeCat} {B : FintypeCat} (e : ↑A ≃ ↑B) (a : ↑B) :

FintypeCat.inv FintypeCat.instCategoryFintypeCat A B (↑FintypeCat.equivEquivIso e) a = ↑e.symm a

source

@[simp]

theorem FintypeCat.equivEquivIso_apply_hom {A : FintypeCat} {B : FintypeCat} (e : ↑A ≃ ↑B) (a : ↑A) :

FintypeCat.hom FintypeCat.instCategoryFintypeCat A B (↑FintypeCat.equivEquivIso e) a = ↑e a

source

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_symm_apply {A : FintypeCat} {B : FintypeCat} (i : A ≅ B) :

∀ (a : ↑B), ↑(↑FintypeCat.equivEquivIso.symm i).symm a = FintypeCat.inv FintypeCat.instCategoryFintypeCat A B i a

source

def FintypeCat.equivEquivIso {A : FintypeCat} {B : FintypeCat} :

↑A ≃ ↑B ≃ (A ≅ B)

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

Instances For

source

def FintypeCat.Skeleton :

Type u

The "standard" skeleton for FintypeCat. This is the full subcategory of FintypeCat 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}.