mathlib documentation

category_theory.fin_category

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.

@[class]
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.

Instances