Mathlib.CategoryTheory.FinCategory.Basic

Module docstring

{"# Finite categories

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

Implementation

Prior to https://github.com/leanprover-community/mathlib4/pull/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. "}

CategoryTheory.discreteFintype instance

{α : Type*} [Fintype α] : Fintype (Discrete α)

Full source

instance discreteFintype {α : Type*} [Fintype α] : Fintype (Discrete α) :=
  Fintype.ofEquiv α discreteEquiv.symm

Finite Objects in Discrete Categories

Informal description

For any finite type $\alpha$, the discrete category on $\alpha$ has finitely many objects.

CategoryTheory.discreteHomFintype instance

{α : Type*} (X Y : Discrete α) : Fintype (X ⟶ Y)

Full source

instance discreteHomFintype {α : Type*} (X Y : Discrete α) : Fintype (X ⟶ Y) := by
  classical
  apply ULift.fintype

Finite Morphism Sets in Discrete Categories

Informal description

For any type $\alpha$ and objects $X, Y$ in the discrete category on $\alpha$, the set of morphisms $\text{Hom}(X, Y)$ is finite.

CategoryTheory.FinCategory structure

(J : Type v) [SmallCategory J]

Full source

/-- A category with a `Fintype` of objects, and a `Fintype` for each morphism space. -/
class FinCategory (J : Type v) [SmallCategory J] where
  fintypeObj : Fintype J := by infer_instance
  fintypeHom : ∀ j j' : J, Fintype (j ⟶ j') := by infer_instance

Finite category

Informal description

A category $\mathcal{J}$ is called *finite* if it has finitely many objects and, for every pair of objects $X, Y \in \mathcal{J}$, the set of morphisms $\text{Hom}(X, Y)$ is finite. This structure is used to represent categories with finite object and morphism sets.

CategoryTheory.finCategoryDiscreteOfFintype instance

(J : Type v) [Fintype J] : FinCategory (Discrete J)

Full source

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

Discrete Categories of Finite Types are Finite

Informal description

For any finite type $J$, the discrete category on $J$ is a finite category.

CategoryTheory.finCategoryOpposite instance

{J : Type v} [SmallCategory J] [FinCategory J] : FinCategory Jᵒᵖ

Full source

/-- The opposite of a finite category is finite.
-/
instance finCategoryOpposite {J : Type v} [SmallCategory J] [FinCategory J] : FinCategory Jᵒᵖ where
  fintypeObj := Fintype.ofEquiv _ equivToOpposite
  fintypeHom j j' := Fintype.ofEquiv _ (opEquiv j j').symm

Opposite of a Finite Category is Finite

Informal description

For any finite category $\mathcal{J}$, the opposite category $\mathcal{J}^\mathrm{op}$ is also finite.

CategoryTheory.finCategoryUlift instance

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

Full source

/-- Applying `ULift` to morphisms and objects of a category preserves finiteness. -/
instance finCategoryUlift {J : Type v} [SmallCategory J] [FinCategory J] :
    FinCategory.{max w v} (ULiftHom.{w, max w v} (ULift.{w, v} J)) where
  fintypeObj := ULift.fintype J
  fintypeHom := fun _ _ => ULift.fintype _

Finiteness Preservation under ULift of Categories

Informal description

For any finite category $\mathcal{J}$, the category obtained by applying the `ULift` functor to both objects and morphisms of $\mathcal{J}$ is also finite.