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

source
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

Instances

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

Instances For

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

Instances For

source
@[instance 100]
instance CategoryTheory.IsIso.of_groupoid {C : Type u} [Groupoid C] {X Y : C} (f : X ⟶ Y) :
IsIso f
source
@[simp]
theorem CategoryTheory.Groupoid.inv_eq_inv {C : Type u} [Groupoid C] {X Y : C} (f : X ⟶ Y) :
inv f = CategoryTheory.inv f
source
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 := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Groupoid.invEquiv_apply {C : Type u} [Groupoid C] {X Y : C} (a✝ : X ⟶ Y) :
invEquiv a✝ = inv a✝
source
@[simp]
theorem CategoryTheory.Groupoid.invEquiv_symm_apply {C : Type u} [Groupoid C] {X Y : C} (a✝ : Y ⟶ X) :
invEquiv.symm a✝ = inv a✝
source
@[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' := ⋯ }

source
@[simp]
theorem CategoryTheory.Groupoid.reverse_eq_inv {C : Type u} [Groupoid C] {X Y : C} (f : X ⟶ Y) :
Quiver.reverse f = inv f
source
instance CategoryTheory.functorMapReverse {C : Type u} [Groupoid C] {D : Type u_1} [Groupoid D] (F : Functor C D) :
F.toPrefunctor.MapReverse
source
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.

Instances For

source
@[simp]
theorem CategoryTheory.Groupoid.isoEquivHom_apply {C : Type u} [Groupoid C] (X Y : C) (self : X ≅ Y) :
(isoEquivHom X Y) self = self.hom
source
@[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
source
@[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
source
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 := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Groupoid.invFunctor_obj (C : Type u) [Groupoid C] (unop : C) :
(invFunctor C).obj unop = Opposite.op unop
source
@[simp]
theorem CategoryTheory.Groupoid.invFunctor_map (C : Type u) [Groupoid C] {x✝ x✝¹ : C} (f : x✝ ⟶ x✝¹) :
(invFunctor C).map f = (inv f).op
source
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

Instances

source
instance CategoryTheory.instIsGroupoid {C : Type u} [Groupoid C] :
IsGroupoid C
source
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 := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

source
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 := ⋯ }

Instances For

source
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
source
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 := ⋯ }

Instances For

source
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)

source
instance CategoryTheory.InducedCategory.isGroupoid {C : Type u} (D : Type u₂) [Category.{v, u₂} D] [IsGroupoid D] (F : C → D) :
IsGroupoid (InducedCategory D F)
source
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 := ⋯ }

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

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

source
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)
source
instance CategoryTheory.isGroupoidProd {α : Type u} {β : Type u₂} [Category.{v, u} α] [Category.{v₂, u₂} β] [IsGroupoid α] [IsGroupoid β] :
IsGroupoid (α × β)
source
theorem CategoryTheory.isGroupoid_iff_isomorphisms_eq_top (C : Type u_1) [Category.{u_2, u_1} C] :
IsGroupoid C ↔ MorphismProperty.isomorphisms C = ⊤