mathlib documentation

category_theory.groupoid

@[class]
structure category_theory.groupoid (obj : Type u) :
Type (max u (v+1))

A groupoid is a category such that all morphisms are isomorphisms.

Instances
@[simp]
theorem category_theory.groupoid.inv_comp {obj : Type u} [c : category_theory.groupoid obj] {X Y : obj} (f : X Y) :
@[simp]
theorem category_theory.groupoid.comp_inv {obj : Type u} [c : category_theory.groupoid obj] {X Y : obj} (f : X Y) :
def category_theory.large_groupoid (C : Type (u+1)) :
Type (u+1)

A large_groupoid is a groupoid where the objects live in Type (u+1) while the morphisms live in Type u.

def category_theory.small_groupoid (C : Type u) :
Type (u+1)

A small_groupoid is a groupoid where the objects and morphisms live in the same universe.

@[instance]
def category_theory.groupoid.iso_equiv_hom {C : Type u} [category_theory.groupoid C] (X Y : C) :
(X Y) (X Y)

In a groupoid, isomorphisms are equivalent to morphisms.

Equations
def category_theory.groupoid.of_is_iso {C : Type u} [category_theory.category C] (all_is_iso : ∀ {X Y : C} (f : X Y), category_theory.is_iso f) :

A category where every morphism is_iso is a groupoid.

Equations