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.

Equations

• CategoryTheory.LargeGroupoid C = CategoryTheory.Groupoid C

@[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.

Equations

• CategoryTheory.SmallGroupoid C = CategoryTheory.Groupoid C

@[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.

Equations

• CategoryTheory.Groupoid.invEquiv = { toFun := CategoryTheory.Groupoid.inv, invFun := CategoryTheory.Groupoid.inv, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[instance 100]

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

Equations

• CategoryTheory.groupoidHasInvolutiveReverse = Quiver.HasInvolutiveReverse.mk ⋯

@[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.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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable 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.

Equations

• CategoryTheory.Groupoid.invFunctor C = { obj := Opposite.op, map := fun {x x_1 : C} (f : x ⟶ x_1) => (CategoryTheory.Groupoid.inv f).op, map_id := ⋯, map_comp := ⋯ }

@[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

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.

Equations

• CategoryTheory.Groupoid.ofIsIso all_is_iso = CategoryTheory.Groupoid.mk (fun {X Y : C} (f : X ⟶ Y) => CategoryTheory.inv f) ⋯ ⋯

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

Equations

• CategoryTheory.Groupoid.ofHomUnique all_unique = CategoryTheory.Groupoid.mk (fun {X Y : C} (x : X ⟶ Y) => default) ⋯ ⋯

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

Equations

• CategoryTheory.InducedCategory.groupoid D F = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y) => CategoryTheory.Groupoid.inv f) ⋯ ⋯

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

Equations

• CategoryTheory.groupoidPi = CategoryTheory.Groupoid.mk (fun {X Y : (i : I) → J i} (f : X ⟶ Y) (i : I) => CategoryTheory.Groupoid.inv (f i)) ⋯ ⋯

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

Equations

• CategoryTheory.groupoidProd = CategoryTheory.Groupoid.mk (fun {X Y : α × β} (f : X ⟶ Y) => (CategoryTheory.Groupoid.inv f.1, CategoryTheory.Groupoid.inv f.2)) ⋯ ⋯