mathlib documentation


Finite categories #

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

Implementation #

Prior to #14046, fin_category required a decidable_eq 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.

@[protected, instance]
noncomputable def category_theory.discrete_hom_fintype {α : Type u_1} (X Y : category_theory.discrete α) :
fintype (X Y)
structure category_theory.fin_category (J : Type v) [category_theory.small_category J] :
Type v
  • fintype_obj : fintype J . "apply_instance"
  • fintype_hom : (Π (j j' : J), fintype (j j')) . "apply_instance"

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

Instances of this typeclass
Instances of other typeclasses for category_theory.fin_category
  • category_theory.fin_category.has_sizeof_inst

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


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