Documentation

Mathlib.CategoryTheory.Groupoid

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 :
Type (max u (v + 1))

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

Instances
    source
    theorem CategoryTheory.Groupoid.inv_comp {obj : Type u} [self : CategoryTheory.Groupoid obj] {X : obj} {Y : obj} (f : X ⟶ Y) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) f = CategoryTheory.CategoryStruct.id Y

    inv f composed f is the identity

    source
    theorem CategoryTheory.Groupoid.comp_inv {obj : Type u} [self : CategoryTheory.Groupoid obj] {X : obj} {Y : obj} (f : X ⟶ Y) :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Groupoid.inv f) = CategoryTheory.CategoryStruct.id X

    f composed with inv f is the identity

    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
    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
    source
    @[instance 100]
    instance CategoryTheory.IsIso.of_groupoid {C : Type u} [CategoryTheory.Groupoid C] {X : C} {Y : C} (f : X ⟶ Y) :
    CategoryTheory.IsIso f
    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem CategoryTheory.Groupoid.inv_eq_inv {C : Type u} [CategoryTheory.Groupoid C] {X : C} {Y : C} (f : X ⟶ Y) :
    CategoryTheory.Groupoid.inv f = CategoryTheory.inv f
    source
    @[simp]
    theorem CategoryTheory.Groupoid.invEquiv_apply {C : Type u} [CategoryTheory.Groupoid C] {X : C} {Y : C} :
    ∀ (a : X ⟶ Y), CategoryTheory.Groupoid.invEquiv a = CategoryTheory.Groupoid.inv a
    source
    @[simp]
    theorem CategoryTheory.Groupoid.invEquiv_symm_apply {C : Type u} [CategoryTheory.Groupoid C] {X : C} {Y : C} :
    ∀ (a : Y ⟶ X), CategoryTheory.Groupoid.invEquiv.symm a = CategoryTheory.Groupoid.inv a
    source
    def CategoryTheory.Groupoid.invEquiv {C : Type u} [CategoryTheory.Groupoid C] {X : C} {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 := ⋯ }
    source
    @[instance 100]
    instance CategoryTheory.groupoidHasInvolutiveReverse {C : Type u} [CategoryTheory.Groupoid C] :
    Quiver.HasInvolutiveReverse C
    Equations
    source
    @[simp]
    theorem CategoryTheory.Groupoid.reverse_eq_inv {C : Type u} [CategoryTheory.Groupoid C] {X : C} {Y : C} (f : X ⟶ Y) :
    Quiver.reverse f = CategoryTheory.Groupoid.inv f
    source
    instance CategoryTheory.functorMapReverse {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (F : CategoryTheory.Functor C D) :
    F.MapReverse
    Equations
    • ⋯ = ⋯
    source
    def CategoryTheory.Groupoid.isoEquivHom {C : Type u} [CategoryTheory.Groupoid C] (X : C) (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.
    source
    @[simp]
    theorem CategoryTheory.Groupoid.invFunctor_map (C : Type u) [CategoryTheory.Groupoid C] :
    ∀ {x x_1 : C} (f : x ⟶ x_1), (CategoryTheory.Groupoid.invFunctor C).map f = (CategoryTheory.Groupoid.inv f).op
    source
    @[simp]
    theorem CategoryTheory.Groupoid.invFunctor_obj (C : Type u) [CategoryTheory.Groupoid C] (unop : C) :
    (CategoryTheory.Groupoid.invFunctor C).obj unop = Opposite.op unop
    source
    noncomputable def CategoryTheory.Groupoid.invFunctor (C : Type u) [CategoryTheory.Groupoid C] :
    CategoryTheory.Functor C Cᵒᵖ

    The functor from a groupoid C to its opposite sending every morphism to its inverse.

    Equations
    source
    noncomputable def CategoryTheory.Groupoid.ofIsIso {C : Type u} [CategoryTheory.Category.{v, u} C] (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso f) :
    CategoryTheory.Groupoid C

    A category where every morphism IsIso is a groupoid.

    Equations
    source
    def CategoryTheory.Groupoid.ofHomUnique {C : Type u} [CategoryTheory.Category.{v, u} C] (all_unique : {X Y : C} → Unique (X ⟶ Y)) :
    CategoryTheory.Groupoid C

    A category with a unique morphism between any two objects is a groupoid

    Equations
    source
    instance CategoryTheory.InducedCategory.groupoid {C : Type u} (D : Type u₂) [CategoryTheory.Groupoid D] (F : C → D) :
    CategoryTheory.Groupoid (CategoryTheory.InducedCategory D F)
    Equations
    source
    instance CategoryTheory.groupoidPi {I : Type u} {J : I → Type u₂} [(i : I) → CategoryTheory.Groupoid (J i)] :
    CategoryTheory.Groupoid ((i : I) → J i)
    Equations
    source
    instance CategoryTheory.groupoidProd {α : Type u} {β : Type v} [CategoryTheory.Groupoid α] [CategoryTheory.Groupoid β] :
    CategoryTheory.Groupoid (α × β)
    Equations