mathlib documentation


Finite categories #

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

Implementation #

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

@[protected, instance]
@[protected, instance]
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.


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


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