Documentation

Mathlib.CategoryTheory.Grothendieck

The Grothendieck construction #

Given a functor F : C ⥤ Cat, the objects of Grothendieck F consist of dependent pairs (b, f), where b : C and f : F.obj c, and a morphism (b, f) ⟶ (b', f') is a pair β : b ⟶ b' in C, and φ : (F.map β).obj f ⟶ f'

Grothendieck.functor makes the Grothendieck construction into a functor from the functor category C ⥤ Cat to the over category Over C in the category of categories.

Categories such as PresheafedSpace are in fact examples of this construction, and it may be interesting to try to generalize some of the development there.

Implementation notes #

Really we should treat Cat as a 2-category, and allow F to be a 2-functor.

There is also a closely related construction starting with G : Cᵒᵖ ⥤ Cat, where morphisms consists again of β : b ⟶ b' and φ : f ⟶ (F.map (op β)).obj f'.

References #

See also CategoryTheory.Functor.Elements for the category of elements of functor F : C ⥤ Type.

The Grothendieck construction (often written as ∫ F in mathematics) for a functor F : C ⥤ Cat gives a category whose

  • base : C

    The underlying object in C

  • fiber : (F.obj self.base)

    The object in the fiber of the base object.

Instances For

    A morphism in the Grothendieck category F : C ⥤ Cat consists of base : X.base ⟶ Y.base and f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber.

    • base : X.base Y.base

      The morphism between base objects.

    • fiber : (F.map self.base).obj X.fiber Y.fiber

      The morphism from the pushforward to the source fiber object to the target fiber object.

    Instances For

      The identity morphism in the Grothendieck category.

      Equations
      Instances For

        Composition of morphisms in the Grothendieck category.

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

          The forgetful functor from Grothendieck F to the source category.

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

            The Grothendieck construction is functorial: a natural transformation α : F ⟶ G induces a functor Grothendieck.map : Grothendieck F ⥤ Grothendieck G.

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

              Making the equality of functors into an isomorphism. Note: we should avoid equality of functors if possible, and we should prefer map_id_iso to map_id_eq whenever we can.

              Equations
              Instances For

                Making the equality of functors into an isomorphism. Note: we should avoid equality of functors if possible, and we should prefer map_comp_iso to map_comp_eq whenever we can.

                Equations
                Instances For

                  The Grothendieck construction as a functor from the functor category E ⥤ Cat to the over category Over E.

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

                    Auxiliary definition for grothendieckTypeToCat, to speed up elaboration.

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

                      Auxiliary definition for grothendieckTypeToCat, to speed up elaboration.

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

                        The Grothendieck construction applied to a functor to Type (thought of as a functor to Cat by realising a type as a discrete category) is the same as the 'category of elements' construction.

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