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.

def FintypeCat : Type (u_1 + 1)

The category of finite types.

Equations

• FintypeCat = CategoryTheory.Bundled Fintype

instance FintypeCat.instCoeSortType : CoeSort FintypeCat (Type u_1)

Equations

• FintypeCat.instCoeSortType = CategoryTheory.Bundled.coeSort

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

Construct a bundled FintypeCat from the underlying type and typeclass.

Equations

• FintypeCat.of X = CategoryTheory.Bundled.of X

instance FintypeCat.instInhabited : Inhabited FintypeCat

Equations

• FintypeCat.instInhabited = { default := FintypeCat.of PEmpty.{?u.3 + 1} }

instance FintypeCat.instFintypeα {X : FintypeCat} : Fintype ↑X

Equations

• FintypeCat.instFintypeα = X.str

instance FintypeCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} FintypeCat

Equations

• FintypeCat.instCategory = CategoryTheory.InducedCategory.category CategoryTheory.Bundled.α

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

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

Equations

• FintypeCat.incl = CategoryTheory.inducedFunctor CategoryTheory.Bundled.α

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

@[simp]

theorem FintypeCat.incl_obj (self : CategoryTheory.Bundled Fintype) : FintypeCat.incl.obj self = ↑self

instance FintypeCat.instFullIncl : FintypeCat.incl.Full

instance FintypeCat.instFaithfulIncl : FintypeCat.incl.Faithful

instance FintypeCat.concreteCategoryFintype : CategoryTheory.ConcreteCategory FintypeCat

Equations

• FintypeCat.concreteCategoryFintype = CategoryTheory.ConcreteCategory.mk FintypeCat.incl

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

@[simp]

theorem FintypeCat.id_apply (X : FintypeCat) (x : ↑X) : CategoryTheory.CategoryStruct.id X x = x

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FintypeCat.equivEquivIso_apply_inv {A B : FintypeCat} (e : ↑A ≃ ↑B) (a : ↑B) : (FintypeCat.equivEquivIso e).inv a = e.symm a

@[simp]

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

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_apply {A B : FintypeCat} (i : A ≅ B) (a✝ : ↑A) : (FintypeCat.equivEquivIso.symm i) a✝ = i.hom a✝

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_symm_apply {A B : FintypeCat} (i : A ≅ B) (a✝ : ↑B) : (FintypeCat.equivEquivIso.symm i).symm a✝ = 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 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

• FintypeCat.Skeleton = ULift.{?u.3, 0} ℕ

def FintypeCat.Skeleton.mk : ℕ → FintypeCat.Skeleton

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

Equations

• FintypeCat.Skeleton.mk = ULift.up

instance FintypeCat.Skeleton.instInhabited : Inhabited FintypeCat.Skeleton

Equations

• FintypeCat.Skeleton.instInhabited = { default := FintypeCat.Skeleton.mk 0 }

def FintypeCat.Skeleton.len : FintypeCat.Skeleton → ℕ

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

Equations

• FintypeCat.Skeleton.len = ULift.down

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

instance FintypeCat.Skeleton.instSmallCategory : CategoryTheory.SmallCategory FintypeCat.Skeleton

Equations

• One or more equations did not get rendered due to their size.

theorem FintypeCat.Skeleton.is_skeletal : CategoryTheory.Skeletal FintypeCat.Skeleton

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

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

Equations

• One or more equations did not get rendered due to their size.

instance FintypeCat.Skeleton.instFullIncl : FintypeCat.Skeleton.incl.Full

instance FintypeCat.Skeleton.instFaithfulIncl : FintypeCat.Skeleton.incl.Faithful

instance FintypeCat.Skeleton.instEssSurjIncl : FintypeCat.Skeleton.incl.EssSurj

instance FintypeCat.Skeleton.instIsEquivalenceIncl : FintypeCat.Skeleton.incl.IsEquivalence

noncomputable def FintypeCat.Skeleton.equivalence : FintypeCat.Skeleton ≌ FintypeCat

The equivalence between Fintype.Skeleton and Fintype.

Equations

• FintypeCat.Skeleton.equivalence = FintypeCat.Skeleton.incl.asEquivalence

@[simp]

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

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

Fintype.Skeleton is a skeleton of Fintype.

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)).

Equations

• One or more equations did not get rendered due to their size.

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

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}.

Equations

• X.uSwitchEquiv = Equiv.ulift.trans (Fintype.equivFin ↑X).symm

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

theorem FintypeCat.uSwitchEquiv_symm_naturality {X Y : FintypeCat} (f : X ⟶ Y) (x : ↑X) : FintypeCat.uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (f x)

theorem FintypeCat.uSwitch_map_uSwitch_map {X Y : FintypeCat} (f : X ⟶ Y) : FintypeCat.uSwitch.map (FintypeCat.uSwitch.map f) = CategoryTheory.CategoryStruct.comp (FintypeCat.equivEquivIso ((FintypeCat.uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).hom (CategoryTheory.CategoryStruct.comp f (FintypeCat.equivEquivIso ((FintypeCat.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}.

Equations

• One or more equations did not get rendered due to their size.

instance FintypeCat.instIsEquivalenceUSwitch : FintypeCat.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)) : σ.app Y (F.map f x) = G.map f (σ.app X x)