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 = { reverse' := fun {a b : C} (f : a ⟶ b) => CategoryTheory.Groupoid.inv f, inv' := ⋯ }

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

@[simp]

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

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

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

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.

Equations

• CategoryTheory.Groupoid.ofIsGroupoid = { toCategory := inst✝¹, inv := fun {X Y : C} (f : X ⟶ Y) => CategoryTheory.inv f, inv_comp := ⋯, comp_inv := ⋯ }

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 = { toCategory := inst✝, inv := fun {X Y : C} (f : X ⟶ Y) => CategoryTheory.inv f, inv_comp := ⋯, comp_inv := ⋯ }

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 = { toCategory := inst✝, inv := fun {X Y : C} (x : X ⟶ Y) => default, inv_comp := ⋯, comp_inv := ⋯ }

theorem CategoryTheory.isGroupoid_of_reflects_iso {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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

Equations

• CategoryTheory.Groupoid.ofFullyFaithfulToGroupoid F h = { toCategory := 𝒞, inv := fun {X Y : C} (f : X ⟶ Y) => h.preimage (CategoryTheory.Groupoid.inv (F.map f)), inv_comp := ⋯, comp_inv := ⋯ }

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.ofFullyFaithfulToGroupoid (CategoryTheory.inducedFunctor F) (CategoryTheory.fullyFaithfulInducedFunctor 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)

Equations

• CategoryTheory.groupoidPi = { toCategory := CategoryTheory.pi J, inv := fun {X Y : (i : I) → J i} (f : X ⟶ Y) (i : I) => CategoryTheory.Groupoid.inv (f i), inv_comp := ⋯, comp_inv := ⋯ }

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

Equations

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

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 (α × β)