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.

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

    f composed with inv f is the identity

    @[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
    Instances For
      @[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
      Instances For
        @[instance 100]
        Equations
        • =
        @[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
        @[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
        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 := }
        Instances For
          @[instance 100]
          Equations
          Equations
          • =
          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.
          Instances For

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

            Equations
            Instances For
              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) :

              A category where every morphism IsIso is a groupoid.

              Equations
              Instances For

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

                Equations
                Instances For
                  instance CategoryTheory.groupoidPi {I : Type u} {J : IType u₂} [(i : I) → CategoryTheory.Groupoid (J i)] :
                  CategoryTheory.Groupoid ((i : I) → J i)
                  Equations
                  Equations