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]
Equations
- category_theory.discrete_fintype = id _inst_1
@[protected, 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.
Instances
- category_theory.fin_category_discrete_of_decidable_fintype
- category_theory.fin_category.as_type_fin_category
- category_theory.limits.walking_parallel_pair.category_theory.fin_category
- category_theory.limits.fin_category_wide_pullback
- category_theory.limits.fin_category_wide_pushout
- category_theory.bicone_fin_category
@[protected, 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'}
@[nolint]
def
category_theory.fin_category.obj_as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
Type
A fin_category α is equivalent to a category with objects in Type.
noncomputable
def
category_theory.fin_category.obj_as_type_equiv
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
The constructed category is indeed equivalent to α.
@[nolint]
def
category_theory.fin_category.as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
Type
A fin_category α is equivalent to a fin_category with in Type.
theorem
category_theory.fin_category.category_as_type_hom
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α]
(i j : category_theory.fin_category.as_type α) :
(i ⟶ j) = fin (fintype.card (i ⟶ j))
@[protected, instance]
noncomputable
def
category_theory.fin_category.category_as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
Equations
- category_theory.fin_category.category_as_type α = {to_category_struct := {to_quiver := {hom := λ (i j : category_theory.fin_category.as_type α), fin (fintype.card (i ⟶ j))}, id := λ (i : category_theory.fin_category.as_type α), ⇑(fintype.equiv_fin (i ⟶ i)) (𝟙 i), comp := λ (i j k : category_theory.fin_category.as_type α) (f : i ⟶ j) (g : j ⟶ k), ⇑(fintype.equiv_fin (i ⟶ k)) (⇑((fintype.equiv_fin (i ⟶ j)).symm) f ≫ ⇑((fintype.equiv_fin (j ⟶ k)).symm) g)}, id_comp' := _, comp_id' := _, assoc' := _}
theorem
category_theory.fin_category.category_as_type_comp
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α]
(i j k : category_theory.fin_category.as_type α)
(f : i ⟶ j)
(g : j ⟶ k) :
f ≫ g = ⇑(fintype.equiv_fin (i ⟶ k)) (⇑((fintype.equiv_fin (i ⟶ j)).symm) f ≫ ⇑((fintype.equiv_fin (j ⟶ k)).symm) g)
theorem
category_theory.fin_category.category_as_type_id
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α]
(i : category_theory.fin_category.as_type α) :
noncomputable
def
category_theory.fin_category.obj_as_type_equiv_as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
The constructed category (as_type α) is equivalent to obj_as_type α.
Equations
- category_theory.fin_category.obj_as_type_equiv_as_type α = {functor := {obj := id (category_theory.fin_category.as_type α), map := λ (i j : category_theory.fin_category.as_type α) (f : i ⟶ j), ⇑((fintype.equiv_fin (i ⟶ j)).symm) f, map_id' := _, map_comp' := _}, inverse := {obj := id (category_theory.fin_category.obj_as_type α), map := λ (i j : category_theory.fin_category.obj_as_type α) (f : i ⟶ j), ⇑(fintype.equiv_fin (i ⟶ j)) f, map_id' := _, map_comp' := _}, unit_iso := category_theory.nat_iso.of_components category_theory.iso.refl _, counit_iso := category_theory.nat_iso.of_components category_theory.iso.refl _, functor_unit_iso_comp' := _}
@[protected, instance]
noncomputable
def
category_theory.fin_category.as_type_fin_category
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
Equations
- category_theory.fin_category.as_type_fin_category α = {decidable_eq_obj := λ (a b : category_theory.fin_category.as_type α), subtype.decidable_eq a b, fintype_obj := fin.fintype (fintype.card α), decidable_eq_hom := λ (j j' : category_theory.fin_category.as_type α) (a b : j ⟶ j'), subtype.decidable_eq a b, fintype_hom := λ (j j' : category_theory.fin_category.as_type α), fin.fintype (fintype.card (j ⟶ j'))}
noncomputable
def
category_theory.fin_category.equiv_as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
The constructed category (as_type α) is indeed equivalent to α.
def
category_theory.fin_category_opposite
{J : Type v}
[category_theory.small_category J]
[category_theory.fin_category J] :
The opposite of a finite category is finite.
Equations
- category_theory.fin_category_opposite = {decidable_eq_obj := opposite.equiv_to_opposite.symm.decidable_eq (λ (a b : J), category_theory.fin_category.decidable_eq_obj a b), fintype_obj := fintype.of_equiv J opposite.equiv_to_opposite, decidable_eq_hom := λ (j j' : Jᵒᵖ), (category_theory.op_equiv j j').decidable_eq, fintype_hom := λ (j j' : Jᵒᵖ), fintype.of_equiv (opposite.unop j' ⟶ opposite.unop j) (category_theory.op_equiv j j').symm}