The category of finite types.

We define the category of finite types, denoted FintypeCat as the full subcategory of types with a Finite 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.

@[reducible, inline]

abbrev FintypeCat : Type (u_1 + 1)

The category of finite types.

@[reducible, inline]

abbrev FintypeCat.of (X : Type u_1) [Finite X] : FintypeCat

Construct a term of FintypeCat from a type endowed with a Finite instance.

@[implicit_reducible]

instance FintypeCat.instCoeSort : CoeSort FintypeCat (Type u_1)

@[implicit_reducible]

instance FintypeCat.instInhabited : Inhabited FintypeCat

instance FintypeCat.instFiniteObj {X : FintypeCat} : Finite X.obj

@[implicit_reducible]

noncomputable def FintypeCat.fintype {X : FintypeCat} : Fintype X.obj

A Fintype instance on objects on FintypeCat, that should be turned on as needed. Prefer the Finite instance if possible.

@[reducible, inline]

abbrev FintypeCat.incl : CategoryTheory.Functor FintypeCat (Type u_1)

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

@[simp]

theorem FintypeCat.incl_map {X✝ Y✝ : CategoryTheory.InducedCategory (Type u_1) CategoryTheory.ObjectProperty.FullSubcategory.obj} (f : X✝ ⟶ Y✝) (a✝ : X✝.obj) : incl.map f a✝ = f.hom a✝

@[simp]

theorem FintypeCat.incl_obj (self : CategoryTheory.ObjectProperty.FullSubcategory Finite) : incl.obj self = self.obj

instance FintypeCat.instFullIncl : incl.Full

instance FintypeCat.instFaithfulIncl : incl.Faithful

@[implicit_reducible]

instance FintypeCat.concreteCategoryFintype : CategoryTheory.ConcreteCategory FintypeCat fun (X Y : FintypeCat) => X.obj ⟶ Y.obj

instance FintypeCat.instFullForgetHomObjFinite : (CategoryTheory.forget FintypeCat).Full

@[simp]

theorem FintypeCat.id_apply (X : FintypeCat) (x : X.obj) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem FintypeCat.comp_apply {X Y Z : FintypeCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X.obj) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

@[simp]

theorem FintypeCat.hom_apply {X Y : FintypeCat} (f : X ⟶ Y) (x : X.obj) : f.hom x = (CategoryTheory.ConcreteCategory.hom f) x

theorem FintypeCat.hom_inv_id_apply {X Y : FintypeCat} (f : X ≅ Y) (x : X.obj) : (CategoryTheory.ConcreteCategory.hom f.inv) ((CategoryTheory.ConcreteCategory.hom f.hom) x) = x

theorem FintypeCat.inv_hom_id_apply {X Y : FintypeCat} (f : X ≅ Y) (y : Y.obj) : (CategoryTheory.ConcreteCategory.hom f.hom) ((CategoryTheory.ConcreteCategory.hom f.inv) y) = y

theorem FintypeCat.hom_ext {X Y : FintypeCat} (f g : X ⟶ Y) (h : ∀ (x : X.obj), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem FintypeCat.hom_ext_iff {X Y : FintypeCat} {f g : X ⟶ Y} : f = g ↔ ∀ (x : X.obj), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

def FintypeCat.homMk {X Y : FintypeCat} (f : X.obj → Y.obj) : X ⟶ Y

Constructor for morphisms in FintypeCat.

@[simp]

theorem FintypeCat.homMk_apply {X Y : FintypeCat} (f : X.obj → Y.obj) (x : X.obj) : (CategoryTheory.ConcreteCategory.hom (homMk f)) x = f x

@[simp]

theorem FintypeCat.id_hom (X : FintypeCat) : CategoryTheory.CategoryStruct.id X.obj = id

@[simp]

theorem FintypeCat.comp_hom {X Y Z : FintypeCat} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom g.hom = g.hom ∘ f.hom

theorem FintypeCat.comp_hom_assoc {X Y Z : FintypeCat} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : Type u_1} (h : Z.obj ⟶ Z✝) : CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h) = CategoryTheory.CategoryStruct.comp (g.hom ∘ f.hom) h

@[simp]

theorem FintypeCat.homMk_eq_id_iff {X : FintypeCat} (f : X.obj → X.obj) : homMk f = CategoryTheory.CategoryStruct.id X ↔ f = id

@[simp]

theorem FintypeCat.homMk_eq_comp_iff {X Y Z : FintypeCat} (f : X.obj → Y.obj) (g : Y.obj → Z.obj) (h : X.obj → Z.obj) : homMk h = CategoryTheory.CategoryStruct.comp (homMk f) (homMk g) ↔ h = g ∘ f

def FintypeCat.equivEquivIso {A B : FintypeCat} : A.obj ≃ B.obj ≃ (A ≅ B)

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

@[simp]

theorem FintypeCat.equivEquivIso_apply_inv {A B : FintypeCat} (e : A.obj ≃ B.obj) : (equivEquivIso e).inv = homMk ⇑e.symm

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_apply {A B : FintypeCat} (i : A ≅ B) (a : A.obj) : (equivEquivIso.symm i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a

@[simp]

theorem FintypeCat.equivEquivIso_apply_hom {A B : FintypeCat} (e : A.obj ≃ B.obj) : (equivEquivIso e).hom = homMk ⇑e

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_symm_apply {A B : FintypeCat} (i : A ≅ B) (a : B.obj) : (equivEquivIso.symm i).symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a

instance FintypeCat.instFiniteHom (X Y : FintypeCat) : Finite (X ⟶ Y)

instance FintypeCat.instFiniteIso (X Y : FintypeCat) : Finite (X ≅ Y)

instance FintypeCat.instFiniteAut (X : FintypeCat) : Finite (CategoryTheory.Aut X)

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 FintypeCat.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 FintypeCat.{u}.

def FintypeCat.Skeleton.mk : ℕ → Skeleton

Given any natural number n, this creates the associated object of FintypeCat.Skeleton.

@[implicit_reducible]

instance FintypeCat.Skeleton.instInhabited : Inhabited Skeleton

def FintypeCat.Skeleton.len : Skeleton → ℕ

Given any object of FintypeCat.Skeleton, this returns the associated natural number.

theorem FintypeCat.Skeleton.ext (X Y : Skeleton) : X.len = Y.len → X = Y

theorem FintypeCat.Skeleton.ext_iff {X Y : Skeleton} : X = Y ↔ X.len = Y.len

@[implicit_reducible]

instance FintypeCat.Skeleton.instSmallCategory : CategoryTheory.SmallCategory Skeleton

theorem FintypeCat.Skeleton.is_skeletal : CategoryTheory.Skeletal Skeleton

def FintypeCat.Skeleton.incl : CategoryTheory.Functor Skeleton FintypeCat

The canonical fully faithful embedding of FintypeCat.Skeleton into FintypeCat.

instance FintypeCat.Skeleton.instFullIncl : incl.Full

instance FintypeCat.Skeleton.instFaithfulIncl : incl.Faithful

instance FintypeCat.Skeleton.instEssSurjIncl : incl.EssSurj

instance FintypeCat.Skeleton.instIsEquivalenceIncl : incl.IsEquivalence

noncomputable def FintypeCat.Skeleton.equivalence : Skeleton ≌ FintypeCat

The equivalence between FintypeCat.Skeleton and FintypeCat.

@[simp]

theorem FintypeCat.Skeleton.incl_mk_nat_card (n : ℕ) : Fintype.card (incl.obj (mk n)).obj = n

theorem FintypeCat.isSkeleton : CategoryTheory.IsSkeletonOf FintypeCat Skeleton Skeleton.incl

FintypeCat.Skeleton is a skeleton of FintypeCat.

noncomputable def FintypeCat.uSwitch : CategoryTheory.Functor FintypeCat FintypeCat

If u and v are two arbitrary universes, we may construct a functor uSwitch.{u, v} : FintypeCat.{u} ⥤ FintypeCat.{v} by sending X : FintypeCat.{u} to ULift.{v} (Fin (Fintype.card X)).

noncomputable def FintypeCat.uSwitchEquiv (X : FintypeCat) : (uSwitch.obj X).obj ≃ X.obj

Switching the universe of an object X : FintypeCat.{u} does not change X up to equivalence of types. This is natural in the sense that it commutes with uSwitch.map f for any f : X ⟶ Y in FintypeCat.{u}.

theorem FintypeCat.uSwitchEquiv_naturality {X Y : FintypeCat} (f : X ⟶ Y) (x : (uSwitch.obj X).obj) : (CategoryTheory.ConcreteCategory.hom f) (X.uSwitchEquiv x) = Y.uSwitchEquiv ((CategoryTheory.ConcreteCategory.hom (uSwitch.map f)) x)

theorem FintypeCat.uSwitchEquiv_symm_naturality {X Y : FintypeCat} (f : X ⟶ Y) (x : X.obj) : (CategoryTheory.ConcreteCategory.hom (uSwitch.map f)) (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm ((CategoryTheory.ConcreteCategory.hom f) x)

theorem FintypeCat.uSwitch_map_uSwitch_map {X Y : FintypeCat} (f : X ⟶ Y) : uSwitch.map (uSwitch.map f) = CategoryTheory.CategoryStruct.comp (equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).hom (CategoryTheory.CategoryStruct.comp f (equivEquivIso ((uSwitch.obj Y).uSwitchEquiv.trans Y.uSwitchEquiv)).inv)

noncomputable def FintypeCat.uSwitchEquivalence : FintypeCat ≌ FintypeCat

uSwitch.{u, v} is an equivalence of categories with quasi-inverse uSwitch.{v, u}.

instance FintypeCat.instIsEquivalenceUSwitch : uSwitch.IsEquivalence

theorem FunctorToFintypeCat.naturality {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C FintypeCat) {X Y : C} (σ : F ⟶ G) (f : X ⟶ Y) (x : (F.obj X).obj) : (CategoryTheory.ConcreteCategory.hom (σ.app Y)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = (CategoryTheory.ConcreteCategory.hom (G.map f)) ((CategoryTheory.ConcreteCategory.hom (σ.app X)) x)