# mathlibdocumentation

category_theory.groupoid

# Groupoids #

We define groupoid as a typeclass extending category, asserting that all morphisms have inverses.

The instance is_iso.of_groupoid (f : X ⟶ Y) : is_iso f means that you can then write inv f to access the inverse of any morphism f.

groupoid.iso_equiv_hom : (X ≅ Y) ≃ (X ⟶ Y) provides the equivalence between isomorphisms and morphisms in a groupoid.

We provide a (non-instance) constructor groupoid.of_is_iso from an existing category with is_iso f for every f.

See also category_theory.core for the groupoid of isomorphisms in a category.

@[class]
structure category_theory.groupoid (obj : Type u) :
Type (max u (v+1))
• to_category :
• inv : Π {X Y : obj}, (X Y)(Y X)
• inv_comp' : (∀ {X Y : obj} (f : X Y), = 𝟙 Y) . "obviously"
• comp_inv' : (∀ {X Y : obj} (f : X Y), = 𝟙 X) . "obviously"

A groupoid is a category such that all morphisms are isomorphisms.

Instances of this typeclass
Instances of other typeclasses for category_theory.groupoid
• category_theory.groupoid.has_sizeof_inst
@[simp]
theorem category_theory.groupoid.inv_comp {obj : Type u} [self : category_theory.groupoid obj] {X Y : obj} (f : X Y) :
@[simp]
theorem category_theory.groupoid.comp_inv {obj : Type u} [self : category_theory.groupoid obj] {X Y : obj} (f : X Y) :
@[reducible]
def category_theory.large_groupoid (C : Type (u+1)) :
Type (u+1)

A large_groupoid is a groupoid where the objects live in Type (u+1) while the morphisms live in Type u.

@[reducible]
def category_theory.small_groupoid (C : Type u) :
Type (u+1)

A small_groupoid is a groupoid where the objects and morphisms live in the same universe.

@[protected, instance]
def category_theory.is_iso.of_groupoid {C : Type u} {X Y : C} (f : X Y) :
def category_theory.groupoid.iso_equiv_hom {C : Type u} (X Y : C) :
(X Y) (X Y)

In a groupoid, isomorphisms are equivalent to morphisms.

Equations
noncomputable def category_theory.groupoid.of_is_iso {C : Type u} (all_is_iso : ∀ {X Y : C} (f : X Y), ) :

A category where every morphism is_iso is a groupoid.

Equations
def category_theory.groupoid.of_hom_unique {C : Type u} (all_unique : Π {X Y : C}, unique (X Y)) :

A category with a unique morphism between any two objects is a groupoid

Equations
@[protected, instance]
def category_theory.induced_category.groupoid {C : Type u} (D : Type u₂) (F : C → D) :
Equations
@[protected, instance]
def category_theory.groupoid_pi {I : Type u} {J : I → Type u₂} [Π (i : I), ] :
category_theory.groupoid (Π (i : I), J i)
Equations
@[protected, instance]
def category_theory.groupoid_prod {α : Type u} {β : Type v}  :
Equations