mathlib documentation


Finite categories

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


We also ask for decidable equality of objects and morphisms, but it may be reasonable to just go classical in future.

structure category_theory.fin_category (J : Type v) [category_theory.small_category J] :
Type v
  • decidable_eq_obj : decidable_eq J . "apply_instance"
  • fintype_obj : fintype J . "apply_instance"
  • decidable_eq_hom : (Π (j j' : J), decidable_eq (j 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.