# mathlibdocumentation

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.

@[instance]
def category_theory.discrete_fintype {α : Type u_1} [fintype α] :

Equations
@[instance]

Equations
@[class]
structure category_theory.fin_category (J : Type v)  :
Type v
• decidable_eq_obj : . "apply_instance"
• fintype_obj : . "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
@[instance]

Equations