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.

structure FintypeCat : Type (u_1 + 1)

The category of finite types.

• of :: (
• carrier : Type u_1

  The underlying type.

• str : Fintype self.carrier
• )

instance FintypeCat.instCoeSort : CoeSort FintypeCat (Type u_1)

Equations

• FintypeCat.instCoeSort = { coe := FintypeCat.carrier }

instance FintypeCat.instInhabited : Inhabited FintypeCat

Equations

• FintypeCat.instInhabited = { default := { carrier := PEmpty.{?u.2 + 1}, str := Fintype.instPEmpty } }

instance FintypeCat.instFintypeCarrier {X : FintypeCat} : Fintype X.carrier

Equations

• FintypeCat.instFintypeCarrier = X.str

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

Equations

• FintypeCat.instCategory = CategoryTheory.InducedCategory.category FintypeCat.carrier

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 FintypeCat.carrier

@[simp]

theorem FintypeCat.incl_obj (self : FintypeCat) : incl.obj self = self.carrier

@[simp]

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

instance FintypeCat.instFullIncl : incl.Full

instance FintypeCat.instFaithfulIncl : incl.Faithful

instance FintypeCat.instFunLikeHomCarrier (X Y : FintypeCat) : FunLike (X ⟶ Y) X.carrier Y.carrier

Equations

• X.instFunLikeHomCarrier Y = { coe := fun (f : X ⟶ Y) => f, coe_injective' := ⋯ }

instance FintypeCat.concreteCategoryFintype : CategoryTheory.ConcreteCategory FintypeCat fun (x1 x2 : FintypeCat) => x1 ⟶ x2

Equations

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

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

@[simp]

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

@[simp]

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

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

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

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

theorem FintypeCat.hom_ext_iff {X Y : FintypeCat} {f g : X ⟶ Y} : f = g ↔ ∀ (x : X.carrier), f x = g x

def FintypeCat.equivEquivIso {A B : FintypeCat} : A.carrier ≃ B.carrier ≃ (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.carrier ≃ B.carrier) (a : B.carrier) : (equivEquivIso e).inv a = e.symm a

@[simp]

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

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_symm_apply {A B : FintypeCat} (i : A ≅ B) (a✝ : B.carrier) : (equivEquivIso.symm i).symm a✝ = i.inv a✝

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_apply {A B : FintypeCat} (i : A ≅ B) (a✝ : A.carrier) : (equivEquivIso.symm i) a✝ = i.hom 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.2, 0} ℕ

def FintypeCat.Skeleton.mk : ℕ → 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 Skeleton

Equations

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

def FintypeCat.Skeleton.len : 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 : Skeleton) : X.len = Y.len → X = Y

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

instance FintypeCat.Skeleton.instSmallCategory : CategoryTheory.SmallCategory Skeleton

Equations

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

theorem FintypeCat.Skeleton.is_skeletal : CategoryTheory.Skeletal Skeleton

def FintypeCat.Skeleton.incl : CategoryTheory.Functor 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 : 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 Fintype.Skeleton and Fintype.

Equations

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

@[simp]

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

theorem FintypeCat.isSkeleton : CategoryTheory.IsSkeletonOf FintypeCat Skeleton 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) : (uSwitch.obj X).carrier ≃ X.carrier

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

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

theorem FintypeCat.uSwitchEquiv_symm_naturality {X Y : FintypeCat} (f : X ⟶ Y) (x : X.carrier) : uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (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}.

Equations

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

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