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.instCoeSortFintypeCatType : CoeSort FintypeCat (Type u_1)

Equations

• FintypeCat.instCoeSortFintypeCatType = 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.instInhabitedFintypeCat : Inhabited FintypeCat

Equations

• FintypeCat.instInhabitedFintypeCat = { default := FintypeCat.of PEmpty.{u_1 + 1} }

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

Equations

• FintypeCat.instFintypeα = X.str

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

Equations

• FintypeCat.instCategoryFintypeCat = CategoryTheory.InducedCategory.category 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

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

instance FintypeCat.instFullFintypeCatInstCategoryFintypeCatTypeTypesIncl : CategoryTheory.Functor.Full FintypeCat.incl

Equations

• FintypeCat.instFullFintypeCatInstCategoryFintypeCatTypeTypesIncl = CategoryTheory.InducedCategory.full CategoryTheory.Bundled.α

instance FintypeCat.instFaithfulFintypeCatInstCategoryFintypeCatTypeTypesIncl : CategoryTheory.Functor.Faithful FintypeCat.incl

Equations

• FintypeCat.instFaithfulFintypeCatInstCategoryFintypeCatTypeTypesIncl = ⋯

instance FintypeCat.concreteCategoryFintype : CategoryTheory.ConcreteCategory FintypeCat

Equations

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

instance FintypeCat.instFullFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype : CategoryTheory.Functor.Full (CategoryTheory.forget FintypeCat)

Equations

• FintypeCat.instFullFintypeCatInstCategoryFintypeCatTypeTypesForgetConcreteCategoryFintype = inferInstanceAs (CategoryTheory.Functor.Full FintypeCat.incl)

@[simp]

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

@[simp]

theorem FintypeCat.comp_apply {X : FintypeCat} {Y : FintypeCat} {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 : FintypeCat} {Y : FintypeCat} (f : X ≅ Y) (x : ↑X) : f.inv (f.hom x) = x

@[simp]

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

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

@[simp]

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

@[simp]

theorem FintypeCat.equivEquivIso_symm_apply_symm_apply {A : FintypeCat} {B : FintypeCat} (i : A ≅ B) : ∀ (a : ↑B), (FintypeCat.equivEquivIso.symm i).symm a = i.inv a

@[simp]

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

@[simp]

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

def FintypeCat.equivEquivIso {A : FintypeCat} {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.

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, 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.instInhabitedSkeleton : Inhabited FintypeCat.Skeleton

Equations

• FintypeCat.Skeleton.instInhabitedSkeleton = { 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 : FintypeCat.Skeleton) (Y : FintypeCat.Skeleton) : FintypeCat.Skeleton.len X = FintypeCat.Skeleton.len Y → X = Y

instance FintypeCat.Skeleton.instSmallCategorySkeleton : 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.instFullSkeletonInstSmallCategorySkeletonFintypeCatInstCategoryFintypeCatIncl : CategoryTheory.Functor.Full FintypeCat.Skeleton.incl

Equations

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

instance FintypeCat.Skeleton.instFaithfulSkeletonInstSmallCategorySkeletonFintypeCatInstCategoryFintypeCatIncl : CategoryTheory.Functor.Faithful FintypeCat.Skeleton.incl

Equations

• FintypeCat.Skeleton.instFaithfulSkeletonInstSmallCategorySkeletonFintypeCatInstCategoryFintypeCatIncl = ⋯

instance FintypeCat.Skeleton.instEssSurjSkeletonFintypeCatInstSmallCategorySkeletonInstCategoryFintypeCatIncl : CategoryTheory.Functor.EssSurj FintypeCat.Skeleton.incl

Equations

• FintypeCat.Skeleton.instEssSurjSkeletonFintypeCatInstSmallCategorySkeletonInstCategoryFintypeCatIncl = ⋯

noncomputable instance FintypeCat.Skeleton.instIsEquivalenceSkeletonInstSmallCategorySkeletonFintypeCatInstCategoryFintypeCatIncl : CategoryTheory.Functor.IsEquivalence FintypeCat.Skeleton.incl

Equations

• FintypeCat.Skeleton.instIsEquivalenceSkeletonInstSmallCategorySkeletonFintypeCatInstCategoryFintypeCatIncl = CategoryTheory.Functor.IsEquivalence.ofFullyFaithfullyEssSurj FintypeCat.Skeleton.incl

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

The equivalence between Fintype.Skeleton and Fintype.

Equations

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

@[simp]

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

noncomputable def FintypeCat.isSkeleton : CategoryTheory.IsSkeletonOf FintypeCat FintypeCat.Skeleton FintypeCat.Skeleton.incl

Fintype.Skeleton is a skeleton of Fintype.

Equations

• FintypeCat.isSkeleton = { skel := FintypeCat.Skeleton.is_skeletal, eqv := inferInstance }