Documentation

Mathlib.CategoryTheory.Category.Grpd

Category of groupoids #

This file contains the definition of the category Grpd of all groupoids. In this category objects are groupoids and morphisms are functors between these groupoids.

We also provide two “forgetting” functors: objects : Grpd ⥤ Type and forgetToCat : Grpd ⥤ Cat.

Implementation notes #

Though Grpd is not a concrete category, we use Bundled to define its carrier type.

def CategoryTheory.Grpd :
Type (max (u + 1) u (v + 1))

Category of groupoids

Equations
Instances For

    Construct a bundled Grpd from the underlying type and the typeclass Groupoid.

    Equations
    Instances For

      Functor that gets the set of objects of a groupoid. It is not called forget, because it is not a faithful functor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Forgetting functor to Cat

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Convert arrows in the category of groupoids to functors, which sometimes helps in applying simp lemmas

          Converts identity in the category of groupoids to the functor identity

          Construct the product over an indexed family of groupoids, as a fan.

          Equations
          Instances For

            The product fan over an indexed family of groupoids, is a limit cone.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def CategoryTheory.Grpd.piIsoPi (J : Type u) (f : JCategoryTheory.Grpd) :
              CategoryTheory.Grpd.of ((j : J) → (f j)) ∏ᶜ f

              The product of a family of groupoids is isomorphic to the product object in the category of Groupoids

              Equations
              Instances For