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

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

class CategoryTheory.Groupoid (obj : Type u) extends CategoryTheory.Category.{v, u} obj : Type (max u (v + 1))

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

• Hom : obj → obj → Type 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) : CategoryStruct.comp (CategoryStruct.id X) f = f
• comp_id {X Y : obj} (f : X ⟶ Y) : CategoryStruct.comp f (CategoryStruct.id Y) = f
• assoc {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g) h = CategoryStruct.comp f (CategoryStruct.comp g h)
• inv {X Y : obj} : (X ⟶ Y) → (Y ⟶ X)

  The inverse morphism

• inv_comp {X Y : obj} (f : X ⟶ Y) : CategoryStruct.comp (inv f) f = CategoryStruct.id Y

  inv f composed f is the identity

• comp_inv {X Y : obj} (f : X ⟶ Y) : CategoryStruct.comp f (inv f) = CategoryStruct.id X

  f composed with inv f is the identity

@[reducible, inline]

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.

@[reducible, inline]

abbrev CategoryTheory.SmallGroupoid (C : Type u) : Type (u + 1)

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

@[instance 100]

instance CategoryTheory.IsIso.of_groupoid {C : Type u} [Groupoid C] {X Y : C} (f : X ⟶ Y) : IsIso f

@[simp]

theorem CategoryTheory.Groupoid.inv_eq_inv {C : Type u} [Groupoid C] {X Y : C} (f : X ⟶ Y) : inv f = CategoryTheory.inv f

def CategoryTheory.Groupoid.invEquiv {C : Type u} [Groupoid C] {X Y : C} : (X ⟶ Y) ≃ (Y ⟶ X)

Groupoid.inv is involutive.

@[simp]

theorem CategoryTheory.Groupoid.invEquiv_symm_apply {C : Type u} [Groupoid C] {X Y : C} (a✝ : Y ⟶ X) : invEquiv.symm a✝ = inv a✝

@[simp]

theorem CategoryTheory.Groupoid.invEquiv_apply {C : Type u} [Groupoid C] {X Y : C} (a✝ : X ⟶ Y) : invEquiv a✝ = inv a✝

@[instance 100]

instance CategoryTheory.groupoidHasInvolutiveReverse {C : Type u} [Groupoid C] : Quiver.HasInvolutiveReverse C

@[simp]

theorem CategoryTheory.Groupoid.reverse_eq_inv {C : Type u} [Groupoid C] {X Y : C} (f : X ⟶ Y) : Quiver.reverse f = inv f

instance CategoryTheory.functorMapReverse {C : Type u} [Groupoid C] {D : Type u_1} [Groupoid D] (F : Functor C D) : F.toPrefunctor.MapReverse

def CategoryTheory.Groupoid.isoEquivHom {C : Type u} [Groupoid C] (X Y : C) : (X ≅ Y) ≃ (X ⟶ Y)

In a groupoid, isomorphisms are equivalent to morphisms.

@[simp]

theorem CategoryTheory.Groupoid.isoEquivHom_symm_apply_inv {C : Type u} [Groupoid C] (X Y : C) (f : X ⟶ Y) : ((isoEquivHom X Y).symm f).inv = CategoryTheory.inv f

@[simp]

theorem CategoryTheory.Groupoid.isoEquivHom_symm_apply_hom {C : Type u} [Groupoid C] (X Y : C) (f : X ⟶ Y) : ((isoEquivHom X Y).symm f).hom = f

@[simp]

theorem CategoryTheory.Groupoid.isoEquivHom_apply {C : Type u} [Groupoid C] (X Y : C) (self : X ≅ Y) : (isoEquivHom X Y) self = self.hom

@[deprecated "Use Groupoid.invEquivalence.functor" (since := "2025-12-31")]

def CategoryTheory.Groupoid.invFunctor (C : Type u) [Groupoid C] : Functor C Cᵒᵖ

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

@[simp]

theorem CategoryTheory.Groupoid.invFunctor_obj (C : Type u) [Groupoid C] (unop : C) : (invFunctor C).obj unop = Opposite.op unop

@[simp]

theorem CategoryTheory.Groupoid.invFunctor_map (C : Type u) [Groupoid C] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) : (invFunctor C).map f = (inv f).op

def CategoryTheory.Groupoid.invEquivalence (C : Type u) [Groupoid C] : C ≌ Cᵒᵖ

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

@[simp]

theorem CategoryTheory.Groupoid.invEquivalence_functor_obj (C : Type u) [Groupoid C] (unop : C) : (invEquivalence C).functor.obj unop = Opposite.op unop

@[simp]

theorem CategoryTheory.Groupoid.invEquivalence_inverse_map (C : Type u) [Groupoid C] {x y : Cᵒᵖ} (f : x ⟶ y) : (invEquivalence C).inverse.map f = inv f.unop

@[simp]

theorem CategoryTheory.Groupoid.invEquivalence_inverse_obj (C : Type u) [Groupoid C] (self : Cᵒᵖ) : (invEquivalence C).inverse.obj self = Opposite.unop self

@[simp]

theorem CategoryTheory.Groupoid.invEquivalence_counitIso (C : Type u) [Groupoid C] : (invEquivalence C).counitIso = NatIso.ofComponents (fun (x : Cᵒᵖ) => Iso.refl (({ obj := Opposite.unop, map := fun {x y : Cᵒᵖ} (f : x ⟶ y) => inv f.unop, map_id := ⋯, map_comp := ⋯ }.comp { obj := Opposite.op, map := fun {x x_1 : C} (f : x ⟶ x_1) => (inv f).op, map_id := ⋯, map_comp := ⋯ }).obj x)) ⋯

@[simp]

theorem CategoryTheory.Groupoid.invEquivalence_unitIso (C : Type u) [Groupoid C] : (invEquivalence C).unitIso = NatIso.ofComponents (fun (x : C) => Iso.refl ((Functor.id C).obj x)) ⋯

@[simp]

theorem CategoryTheory.Groupoid.invEquivalence_functor_map (C : Type u) [Groupoid C] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) : (invEquivalence C).functor.map f = (inv f).op

class CategoryTheory.IsGroupoid (C : Type u) [Category.{v, u} C] : Prop

A Prop-valued typeclass asserting that a given category is a groupoid.

• all_isIso {X Y : C} (f : X ⟶ Y) : IsIso f

instance CategoryTheory.instIsGroupoid {C : Type u} [Groupoid C] : IsGroupoid C

noncomputable def CategoryTheory.Groupoid.ofIsGroupoid {C : Type u} [Category.{v, u} C] [IsGroupoid C] : Groupoid C

Promote (noncomputably) an IsGroupoid to a Groupoid structure.

noncomputable def CategoryTheory.Groupoid.ofIsIso {C : Type u} [Category.{v, u} C] (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), IsIso f) : Groupoid C

A category where every morphism IsIso is a groupoid.

def CategoryTheory.Groupoid.ofHomUnique {C : Type u} [Category.{v, u} C] (all_unique : {X Y : C} → Unique (X ⟶ Y)) : Groupoid C

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

theorem CategoryTheory.isGroupoid_of_reflects_iso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.ReflectsIsomorphisms] [IsGroupoid D] : IsGroupoid C

def CategoryTheory.Groupoid.ofFullyFaithfulToGroupoid {C : Type u_1} [𝒞 : Category.{u_2, u_1} C] {D : Type u} [Groupoid D] (F : Functor C D) (h : F.FullyFaithful) : Groupoid C

A category equipped with a fully faithful functor to a groupoid is fully faithful

instance CategoryTheory.InducedCategory.groupoid {C : Type u} (D : Type u₂) [Groupoid D] (F : C → D) : Groupoid (InducedCategory D F)

instance CategoryTheory.InducedCategory.isGroupoid {C : Type u} (D : Type u₂) [Category.{v, u₂} D] [IsGroupoid D] (F : C → D) : IsGroupoid (InducedCategory D F)

instance CategoryTheory.groupoidPi {I : Type u} {J : I → Type u₂} [(i : I) → Groupoid (J i)] : Groupoid ((i : I) → J i)

instance CategoryTheory.groupoidProd {α : Type u} {β : Type v} [Groupoid α] [Groupoid β] : Groupoid (α × β)

instance CategoryTheory.isGroupoidPi {I : Type u} {J : I → Type u₂} [(i : I) → Category.{v, u₂} (J i)] [∀ (i : I), IsGroupoid (J i)] : IsGroupoid ((i : I) → J i)

instance CategoryTheory.isGroupoidProd {α : Type u} {β : Type u₂} [Category.{v, u} α] [Category.{v₂, u₂} β] [IsGroupoid α] [IsGroupoid β] : IsGroupoid (α × β)

theorem CategoryTheory.isGroupoid_iff_isomorphisms_eq_top (C : Type u_1) [Category.{v_1, u_1} C] : IsGroupoid C ↔ MorphismProperty.isomorphisms C = ⊤