Finite categories

A category is finite in this sense if it has finitely many objects, and finitely many morphisms.

Implementation

Prior to #14046, FinCategory required a DecidableEq instance on the object and morphism types. This does not seem to have had any practical payoff (i.e. making some definition constructive) so we have removed these requirements to avoid having to supply instances or delay with non-defeq conflicts between instances.

instance CategoryTheory.discreteFintype {α : Type u_1} [Fintype α] : Fintype (CategoryTheory.Discrete α)

instance CategoryTheory.discreteHomFintype {α : Type u_1} (X : CategoryTheory.Discrete α) (Y : CategoryTheory.Discrete α) : Fintype (X ⟶ Y)

class CategoryTheory.FinCategory (J : Type v) [CategoryTheory.SmallCategory J] : Type v

• fintypeObj : Fintype J
• fintypeHom : (j j' : J) → Fintype (j ⟶ j')

A category with a Fintype of objects, and a Fintype for each morphism space.

instance CategoryTheory.finCategoryDiscreteOfFintype (J : Type v) [Fintype J] : CategoryTheory.FinCategory (CategoryTheory.Discrete J)

@[inline, reducible]

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

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

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

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

The constructed category is indeed equivalent to α.

@[inline, reducible]

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

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

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)

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

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

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

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

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

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

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

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

instance CategoryTheory.finCategoryOpposite {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.FinCategory Jᵒᵖ

The opposite of a finite category is finite.

instance CategoryTheory.finCategoryUlift {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.FinCategory (CategoryTheory.ULiftHom (ULift.{w, v} J))

Applying ULift to morphisms and objects of a category preserves finiteness.