Finite categories are equivalent to category in Type 0.

@[reducible, inline]

abbrev CategoryTheory.FinCategory.ObjAsType (α : Type u_1) [Fintype α] : Type

A FinCategory α is equivalent to a category with objects in Type.

Equations

• CategoryTheory.FinCategory.ObjAsType α = CategoryTheory.InducedCategory α ⇑(Fintype.equivFin α).symm

instance CategoryTheory.FinCategory.instFintypeHomObjAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] {i : CategoryTheory.FinCategory.ObjAsType α} {j : CategoryTheory.FinCategory.ObjAsType α} : Fintype (i ⟶ j)

Equations

• CategoryTheory.FinCategory.instFintypeHomObjAsType α = CategoryTheory.FinCategory.fintypeHom ((Fintype.equivFin α).symm i) ((Fintype.equivFin α).symm j)

noncomputable def CategoryTheory.FinCategory.objAsTypeEquiv (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] : CategoryTheory.FinCategory.ObjAsType α ≌ α

The constructed category is indeed equivalent to α.

Equations

• CategoryTheory.FinCategory.objAsTypeEquiv α = (CategoryTheory.inducedFunctor ⇑(Fintype.equivFin α).symm).asEquivalence

@[reducible, inline]

abbrev CategoryTheory.FinCategory.AsType (α : Type u_1) [Fintype α] : Type

A FinCategory α is equivalent to a fin_category with in Type.

Equations

• CategoryTheory.FinCategory.AsType α = Fin (Fintype.card α)

theorem CategoryTheory.FinCategory.categoryAsType_comp (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] : ∀ {X Y Z : CategoryTheory.FinCategory.AsType α} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = (Fintype.equivFin (X ⟶ Z)) (CategoryTheory.CategoryStruct.comp ((Fintype.equivFin (X ⟶ Y)).symm f) ((Fintype.equivFin (Y ⟶ Z)).symm g))

theorem CategoryTheory.FinCategory.categoryAsType_id (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] (i : CategoryTheory.FinCategory.AsType α) : CategoryTheory.CategoryStruct.id i = (Fintype.equivFin (i ⟶ i)) (CategoryTheory.CategoryStruct.id i)

noncomputable instance CategoryTheory.FinCategory.categoryAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] : CategoryTheory.SmallCategory (CategoryTheory.FinCategory.AsType α)

Equations

• CategoryTheory.FinCategory.categoryAsType α = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.FinCategory.asTypeToObjAsType_map (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] {X : CategoryTheory.FinCategory.AsType α} {Y : CategoryTheory.FinCategory.AsType α} (a : Fin (Fintype.card (X ⟶ Y))) : (CategoryTheory.FinCategory.asTypeToObjAsType α).map a = (Fintype.equivFin (X ⟶ Y)).symm a

@[simp]

theorem CategoryTheory.FinCategory.asTypeToObjAsType_obj (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] (a : CategoryTheory.FinCategory.AsType α) : (CategoryTheory.FinCategory.asTypeToObjAsType α).obj a = id a

noncomputable def CategoryTheory.FinCategory.asTypeToObjAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] : CategoryTheory.Functor (CategoryTheory.FinCategory.AsType α) (CategoryTheory.FinCategory.ObjAsType α)

The "identity" functor from AsType α to ObjAsType α.

Equations

• CategoryTheory.FinCategory.asTypeToObjAsType α = { obj := id, map := fun {X Y : CategoryTheory.FinCategory.AsType α} => ⇑(Fintype.equivFin (X ⟶ Y)).symm, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.FinCategory.objAsTypeToAsType_map (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] {X : CategoryTheory.FinCategory.ObjAsType α} {Y : CategoryTheory.FinCategory.ObjAsType α} (a : X ⟶ Y) : (CategoryTheory.FinCategory.objAsTypeToAsType α).map a = (Fintype.equivFin (X ⟶ Y)) a

@[simp]

theorem CategoryTheory.FinCategory.objAsTypeToAsType_obj (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] (a : CategoryTheory.FinCategory.ObjAsType α) : (CategoryTheory.FinCategory.objAsTypeToAsType α).obj a = id a

noncomputable def CategoryTheory.FinCategory.objAsTypeToAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] : CategoryTheory.Functor (CategoryTheory.FinCategory.ObjAsType α) (CategoryTheory.FinCategory.AsType α)

The "identity" functor from ObjAsType α to AsType α.

Equations

• CategoryTheory.FinCategory.objAsTypeToAsType α = { obj := id, map := fun {X Y : CategoryTheory.FinCategory.ObjAsType α} => ⇑(Fintype.equivFin (X ⟶ Y)), map_id := ⋯, map_comp := ⋯ }

noncomputable def CategoryTheory.FinCategory.asTypeEquivObjAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] : CategoryTheory.FinCategory.AsType α ≌ CategoryTheory.FinCategory.ObjAsType α

The constructed category (AsType α) is equivalent to ObjAsType α.

Equations

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

noncomputable instance CategoryTheory.FinCategory.asTypeFinCategory (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] : CategoryTheory.FinCategory (CategoryTheory.FinCategory.AsType α)

Equations

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

noncomputable def CategoryTheory.FinCategory.equivAsType (α : Type u_1) [Fintype α] [CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α] : CategoryTheory.FinCategory.AsType α ≌ α

The constructed category (ObjAsType α) is indeed equivalent to α.

Equations

• CategoryTheory.FinCategory.equivAsType α = (CategoryTheory.FinCategory.asTypeEquivObjAsType α).trans (CategoryTheory.FinCategory.objAsTypeEquiv α)