@[class]
- to_category : category_theory.category obj
- inv : Π {X Y : obj}, (X ⟶ Y) → (Y ⟶ X)
- inv_comp' : (∀ {X Y : obj} (f : X ⟶ Y), category_theory.groupoid.inv f ≫ f = 𝟙 Y) . "obviously"
- comp_inv' : (∀ {X Y : obj} (f : X ⟶ Y), f ≫ category_theory.groupoid.inv f = 𝟙 X) . "obviously"
A groupoid is a category such that all morphisms are isomorphisms.
@[instance]
def
category_theory.is_iso.of_groupoid
{C : Type u}
[category_theory.groupoid C]
{X Y : C}
(f : X ⟶ Y) :
Equations
- category_theory.is_iso.of_groupoid f = {inv := category_theory.groupoid.inv f, hom_inv_id' := _, inv_hom_id' := _}
In a groupoid, isomorphisms are equivalent to morphisms.
Equations
- category_theory.groupoid.iso_equiv_hom X Y = {to_fun := category_theory.iso.hom Y, inv_fun := λ (f : X ⟶ Y), category_theory.as_iso f, left_inv := _, right_inv := _}
def
category_theory.groupoid.of_is_iso
{C : Type u}
[category_theory.category C]
(all_is_iso : Π {X Y : C} (f : X ⟶ Y), category_theory.is_iso f) :
A category where every morphism is_iso is a groupoid.
Equations
- category_theory.groupoid.of_is_iso all_is_iso = {to_category := {to_category_struct := category_theory.category.to_category_struct _inst_1, id_comp' := _, comp_id' := _, assoc' := _}, inv := λ (X Y : C) (f : X ⟶ Y), category_theory.is_iso.inv f, inv_comp' := _, comp_inv' := _}
def
category_theory.groupoid.of_trunc_split_mono
{C : Type u}
[category_theory.category C]
(all_split_mono : Π {X Y : C} (f : X ⟶ Y), trunc (category_theory.split_mono f)) :
A category where every morphism has a trunc retraction is computably a groupoid.
Equations
- category_theory.groupoid.of_trunc_split_mono all_split_mono = category_theory.groupoid.of_is_iso (λ (X Y : C) (f : X ⟶ Y), (all_split_mono f).rec_on_subsingleton (λ (a : category_theory.split_mono f), (all_split_mono (category_theory.retraction f)).rec_on_subsingleton (λ (a_1 : category_theory.split_mono (category_theory.retraction f)), category_theory.is_iso.of_mono_retraction)))