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.
A Groupoid
is a category such that all morphisms are isomorphisms.
- Hom : obj → obj → Type v
- id : (X : obj) → X ⟶ X
- id_comp : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
- comp_id : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
- assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
The inverse morphism
- inv_comp : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) f = CategoryTheory.CategoryStruct.id Y
inv f
composedf
is the identity - comp_inv : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Groupoid.inv f) = CategoryTheory.CategoryStruct.id X
f
composed withinv f
is the identity
Instances
inv f
composed f
is the identity
f
composed with inv f
is the identity
A LargeGroupoid
is a groupoid
where the objects live in Type (u+1)
while the morphisms live in Type u
.
Equations
Instances For
A SmallGroupoid
is a groupoid
where the objects and morphisms live in the same universe.
Equations
Instances For
Equations
- ⋯ = ⋯
Groupoid.inv
is involutive.
Equations
- CategoryTheory.Groupoid.invEquiv = { toFun := CategoryTheory.Groupoid.inv, invFun := CategoryTheory.Groupoid.inv, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- CategoryTheory.groupoidHasInvolutiveReverse = Quiver.HasInvolutiveReverse.mk ⋯
Equations
- ⋯ = ⋯
In a groupoid, isomorphisms are equivalent to morphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 Y : C} (f : X ⟶ Y) => (CategoryTheory.Groupoid.inv f).op, map_id := ⋯, map_comp := ⋯ }
Instances For
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) ⋯ ⋯
Instances For
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) ⋯ ⋯
Instances For
Equations
- CategoryTheory.InducedCategory.groupoid D F = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y) => CategoryTheory.Groupoid.inv f) ⋯ ⋯
Equations
- CategoryTheory.groupoidPi = CategoryTheory.Groupoid.mk (fun {X Y : (i : I) → J i} (f : X ⟶ Y) (i : I) => CategoryTheory.Groupoid.inv (f i)) ⋯ ⋯
Equations
- CategoryTheory.groupoidProd = CategoryTheory.Groupoid.mk (fun {X Y : α × β} (f : X ⟶ Y) => (CategoryTheory.Groupoid.inv f.1, CategoryTheory.Groupoid.inv f.2)) ⋯ ⋯