# Documentation

Mathlib.CategoryTheory.Groupoid

# Groupoids #

We define Groupoid as a typeclass extending Category, asserting that all morphisms have inverses.

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

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

We provide a (non-instance) constructor Groupoid.ofIsIso from an existing category with IsIso f for every f.

See also CategoryTheory.Core for the groupoid of isomorphisms in a category.

class CategoryTheory.Groupoid (obj : Type u) extends :
Type (max u (v + 1))
• Hom : objobjType v
• id : (X : obj) → X X
• comp : {X Y Z : obj} → (X Y) → (Y Z) → (X Z)
• id_comp : ∀ {X Y : obj} (f : X Y),
• comp_id : ∀ {X Y : obj} (f : X Y),
• assoc : ∀ {W X Y Z : obj} (f : W X) (g : X Y) (h : Y Z),
• inv : {X Y : obj} → (X Y) → (Y X)

The inverse morphism

• inv_comp : ∀ {X Y : obj} (f : X Y),

inv f composed f is the identity

• comp_inv : ∀ {X Y : obj} (f : X Y),

f composed with inv f is the identity

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

Instances
@[inline, reducible]
abbrev CategoryTheory.LargeGroupoid (C : Type (u + 1)) :
Type (u + 1)

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

Instances For
@[inline, reducible]
abbrev CategoryTheory.SmallGroupoid (C : Type u) :
Type (u + 1)

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

Instances For
instance CategoryTheory.IsIso.of_groupoid {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Groupoid.inv_eq_inv {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Groupoid.invEquiv_symm_apply {C : Type u} {X : C} {Y : C} :
∀ (a : Y X), CategoryTheory.Groupoid.invEquiv.symm a =
@[simp]
theorem CategoryTheory.Groupoid.invEquiv_apply {C : Type u} {X : C} {Y : C} :
∀ (a : X Y), CategoryTheory.Groupoid.invEquiv a =
def CategoryTheory.Groupoid.invEquiv {C : Type u} {X : C} {Y : C} :
(X Y) (Y X)

Groupoid.inv is involutive.

Instances For
@[simp]
theorem CategoryTheory.Groupoid.reverse_eq_inv {C : Type u} {X : C} {Y : C} (f : X Y) :
instance CategoryTheory.functorMapReverse {C : Type u} {D : Type u_1} (F : ) :
Prefunctor.MapReverse F.toPrefunctor
def CategoryTheory.Groupoid.isoEquivHom {C : Type u} (X : C) (Y : C) :
(X Y) (X Y)

In a groupoid, isomorphisms are equivalent to morphisms.

Instances For
@[simp]
theorem CategoryTheory.Groupoid.invFunctor_map (C : Type u) {X : C} {Y : C} (f : X Y) :
().map f = ().op
@[simp]
theorem CategoryTheory.Groupoid.invFunctor_obj (C : Type u) (x : C) :
().obj x =
noncomputable def CategoryTheory.Groupoid.invFunctor (C : Type u) :

The functor from a groupoid C to its opposite sending every morphism to its inverse.

Instances For
noncomputable def CategoryTheory.Groupoid.ofIsIso {C : Type u} (all_is_iso : ∀ {X Y : C} (f : X Y), ) :

A category where every morphism IsIso is a groupoid.

Instances For
def CategoryTheory.Groupoid.ofHomUnique {C : Type u} (all_unique : {X Y : C} → Unique (X Y)) :

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

Instances For
instance CategoryTheory.InducedCategory.groupoid {C : Type u} (D : Type u₂) (F : CD) :
instance CategoryTheory.groupoidPi {I : Type u} {J : IType u₂} [(i : I) → ] :
CategoryTheory.Groupoid ((i : I) → J i)