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.
- 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
A Groupoid
is a category such that all morphisms are isomorphisms.
Instances
A LargeGroupoid
is a groupoid
where the objects live in Type (u+1)
while the morphisms live in Type u
.
Instances For
A SmallGroupoid
is a groupoid
where the objects and morphisms live in the same universe.
Instances For
Groupoid.inv
is involutive.
Instances For
In a groupoid, isomorphisms are equivalent to morphisms.
Instances For
The functor from a groupoid C
to its opposite sending every morphism to its inverse.
Instances For
A category where every morphism IsIso
is a groupoid.
Instances For
A category with a unique morphism between any two objects is a groupoid