Category of groupoids
This file contains the definition of the category Groupoid of all groupoids.
In this category objects are groupoids and morphisms are functors
between these groupoids.
We also provide two “forgetting” functors: objects : Groupoid ⥤ Type
and forget_to_Cat : Groupoid ⥤ Cat.
Implementation notes
Though Groupoid is not a concrete category, we use bundled to define
its carrier type.
Category of groupoids
@[instance]
Construct a bundled Groupoid from the underlying type and the typeclass.
Equations
@[instance]
Category structure on Groupoid
Equations
- category_theory.Groupoid.category = {to_category_struct := {to_has_hom := {hom := λ (C D : category_theory.Groupoid), C.α ⥤ D.α}, id := λ (C : category_theory.Groupoid), 𝟭 C.α, comp := λ (C D E : category_theory.Groupoid) (F : C ⟶ D) (G : D ⟶ E), F ⋙ G}, id_comp' := category_theory.Groupoid.category._proof_1, comp_id' := category_theory.Groupoid.category._proof_2, assoc' := category_theory.Groupoid.category._proof_3}
Functor that gets the set of objects of a groupoid. It is not
called forget, because it is not a faithful functor.
Equations
- category_theory.Groupoid.objects = {obj := category_theory.bundled.α category_theory.groupoid, map := λ (C D : category_theory.Groupoid) (F : C ⟶ D), F.obj, map_id' := category_theory.Groupoid.objects._proof_1, map_comp' := category_theory.Groupoid.objects._proof_2}
Forgetting functor to Cat
Equations
- category_theory.Groupoid.forget_to_Cat = {obj := λ (C : category_theory.Groupoid), category_theory.Cat.of C.α, map := λ (C D : category_theory.Groupoid), id, map_id' := category_theory.Groupoid.forget_to_Cat._proof_1, map_comp' := category_theory.Groupoid.forget_to_Cat._proof_2}
@[instance]
Equations
- category_theory.Groupoid.forget_to_Cat_full = {preimage := λ (C D : category_theory.Groupoid), id, witness' := category_theory.Groupoid.forget_to_Cat_full._proof_1}