Finite categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A category is finite in this sense if it has finitely many objects, and finitely many morphisms.
Implementation #
Prior to #14046, fin_category required a decidable_eq instance on the object and morphism types.
This does not seem to have had any practical payoff (i.e. making some definition constructive)
so we have removed these requirements to avoid
having to supply instances or delay with non-defeq conflicts between instances.
@[protected, instance]
@[protected, instance]
noncomputable
def
category_theory.discrete_hom_fintype
{α : Type u_1}
(X Y : category_theory.discrete α) :
Equations
- category_theory.discrete_hom_fintype X Y = ulift.fintype (plift (X.as = Y.as))
@[class]
- fintype_obj : fintype 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 of this typeclass
- category_theory.fin_category_discrete_of_fintype
- category_theory.fin_category.as_type_fin_category
- category_theory.fin_category_opposite
- category_theory.fin_category_ulift
- category_theory.limits.walking_parallel_pair.category_theory.fin_category
- category_theory.limits.fin_category_wide_pullback
- category_theory.limits.fin_category_wide_pushout
Instances of other typeclasses for category_theory.fin_category
- category_theory.fin_category.has_sizeof_inst
@[protected, instance]
Equations
- category_theory.fin_category_discrete_of_fintype J = {fintype_obj := category_theory.discrete_fintype _inst_1, fintype_hom := λ (j j' : category_theory.discrete J), category_theory.discrete_hom_fintype j j'}
@[nolint, reducible]
def
category_theory.fin_category.obj_as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
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, reducible]
def
category_theory.fin_category.as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
A fin_category α is equivalent to a fin_category with in Type.
@[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.as_type_to_obj_as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
The "identity" functor from as_type α to obj_as_type α.
Equations
- category_theory.fin_category.as_type_to_obj_as_type α = {obj := id (category_theory.fin_category.as_type α), map := λ (i j : category_theory.fin_category.as_type α), ⇑((fintype.equiv_fin (i ⟶ j)).symm), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.fin_category.as_type_to_obj_as_type_map
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α]
(i j : category_theory.fin_category.as_type α)
(ᾰ : fin (fintype.card (i ⟶ j))) :
(category_theory.fin_category.as_type_to_obj_as_type α).map ᾰ = ⇑((fintype.equiv_fin (i ⟶ j)).symm) ᾰ
@[simp]
theorem
category_theory.fin_category.as_type_to_obj_as_type_obj
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α]
(a : category_theory.fin_category.as_type α) :
@[simp]
theorem
category_theory.fin_category.obj_as_type_to_as_type_obj
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α]
(a : category_theory.fin_category.obj_as_type α) :
noncomputable
def
category_theory.fin_category.obj_as_type_to_as_type
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α] :
The "identity" functor from obj_as_type α to as_type α.
Equations
- category_theory.fin_category.obj_as_type_to_as_type α = {obj := id (category_theory.fin_category.obj_as_type α), map := λ (i j : category_theory.fin_category.obj_as_type α), ⇑(fintype.equiv_fin (i ⟶ j)), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.fin_category.obj_as_type_to_as_type_map
(α : Type u_1)
[fintype α]
[category_theory.small_category α]
[category_theory.fin_category α]
(i j : category_theory.fin_category.obj_as_type α)
(ᾰ : i ⟶ j) :
(category_theory.fin_category.obj_as_type_to_as_type α).map ᾰ = ⇑(fintype.equiv_fin (i ⟶ j)) ᾰ
noncomputable
def
category_theory.fin_category.as_type_equiv_obj_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.as_type_equiv_obj_as_type α = category_theory.equivalence.mk (category_theory.fin_category.as_type_to_obj_as_type α) (category_theory.fin_category.obj_as_type_to_as_type α) (category_theory.nat_iso.of_components category_theory.iso.refl _) (category_theory.nat_iso.of_components category_theory.iso.refl _)
@[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 α = {fintype_obj := fin.fintype (fintype.card α), 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 α.
@[protected, instance]
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 = {fintype_obj := fintype.of_equiv J opposite.equiv_to_opposite, fintype_hom := λ (j j' : Jᵒᵖ), fintype.of_equiv (opposite.unop j' ⟶ opposite.unop j) (category_theory.op_equiv j j').symm}
@[protected, instance]
def
category_theory.fin_category_ulift
{J : Type v}
[category_theory.small_category J]
[category_theory.fin_category J] :
Applying ulift to morphisms and objects of a category preserves finiteness.
Equations
- category_theory.fin_category_ulift = {fintype_obj := ulift.fintype J category_theory.fin_category.fintype_obj, fintype_hom := λ (j j' : category_theory.ulift_hom (ulift J)), ulift.fintype (j.obj_down ⟶ j'.obj_down)}