Documentation

Mathlib.CategoryTheory.Groupoid.Grpd.Basic

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.

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

Category of groupoids

Instances For
    source
    @[implicit_reducible]
    instance CategoryTheory.Grpd.instInhabited :
    Inhabited Grpd
    source
    @[implicit_reducible]
    instance CategoryTheory.Grpd.str' (C : Grpd) :
    Groupoid ↑C
    source
    @[implicit_reducible]
    instance CategoryTheory.Grpd.instCoeSortType :
    CoeSort Grpd (Type u_1)
    source
    def CategoryTheory.Grpd.of (C : Type u) [Groupoid C] :
    Grpd

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

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Grpd.coe_of (C : Type u) [Groupoid C] :
      ↑(of C) = C
      source
      @[implicit_reducible]
      instance CategoryTheory.Grpd.category :
      LargeCategory Grpd

      Category structure on Grpd

      source
      def CategoryTheory.Grpd.objects :
      Functor Grpd (Type u)

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

      Instances For
        source
        def CategoryTheory.Grpd.forgetToCat :
        Functor Grpd Cat

        Forgetting functor to Cat

        Instances For
          source
          @[implicit_reducible]
          instance CategoryTheory.Grpd.instGroupoidαCategoryObjCatForgetToCat (X : Grpd) :
          Groupoid ↑(forgetToCat.obj X)
          source
          instance CategoryTheory.Grpd.forgetToCat_full :
          forgetToCat.Full
          source
          instance CategoryTheory.Grpd.forgetToCat_faithful :
          forgetToCat.Faithful
          source
          theorem CategoryTheory.Grpd.comp_eq_comp {C D E : Grpd} (f : C ⟶ D) (g : D ⟶ E) :
          CategoryStruct.comp f g = Functor.comp f g

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

          source
          theorem CategoryTheory.Grpd.id_eq_id {C : Grpd} :
          CategoryStruct.id C = Functor.id ↑C

          Converts identity in the category of groupoids to the functor identity

          source
          def CategoryTheory.Grpd.piLimitFan ⦃J : Type u⦄ (F : J → Grpd) :
          Limits.Fan F

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

          Instances For
            source
            def CategoryTheory.Grpd.piLimitFanIsLimit ⦃J : Type u⦄ (F : J → Grpd) :
            Limits.IsLimit (piLimitFan F)

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

            Instances For
              source
              instance CategoryTheory.Grpd.has_pi :
              Limits.HasProducts Grpd
              source
              noncomputable def CategoryTheory.Grpd.piIsoPi (J : Type u) (f : J → 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

              Instances For
                source
                @[simp]
                theorem CategoryTheory.Grpd.piIsoPi_hom_π (J : Type u) (f : J → Grpd) (j : J) :
                CategoryStruct.comp (piIsoPi J f).hom (Limits.Pi.π f j) = Pi.eval (fun (i : J) => ↑(f i)) j