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 α] [SmallCategory α] [FinCategory α] {i j : 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 α] [SmallCategory α] : 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 α)

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

Equations

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.FinCategory.asTypeEquivObjAsType (α : Type u_1) [Fintype α] [SmallCategory α] [FinCategory α] : AsType α ≌ 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 α] [SmallCategory α] [FinCategory α] : FinCategory (AsType α)

Equations

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

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

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

Equations

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