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]
Equations
- category_theory.discrete_fintype = id _inst_1
@[instance]
def
category_theory.discrete_hom_fintype
{α : Type u_1}
[decidable_eq α]
(X Y : category_theory.discrete α) :
Equations
- category_theory.discrete_hom_fintype X Y = ulift.fintype (plift (X = Y))
@[class]
- 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.
@[instance]
def
category_theory.fin_category_discrete_of_decidable_fintype
(J : Type v)
[decidable_eq J]
[fintype J] :
Equations
- category_theory.fin_category_discrete_of_decidable_fintype J = {decidable_eq_obj := λ (a b : category_theory.discrete J), _inst_1 a b, fintype_obj := category_theory.discrete_fintype _inst_2, decidable_eq_hom := λ (j j' : category_theory.discrete J) (a b : j ⟶ j'), ulift.decidable_eq a b, fintype_hom := λ (j j' : category_theory.discrete J), category_theory.discrete_hom_fintype j j'}