Documentation

Mathlib.CategoryTheory.Bicategory.Grothendieck

The Grothendieck and CoGrothendieck constructions #

The Grothendieck construction #

Given a category 𝒮 and any pseudofunctor F from 𝒮 to Cat, we associate to it a category ∫ F, defined as follows:

The category ∫ F is equipped with a projection functor ∫ F ⥤ 𝒮, given by projecting to the first factors, i.e.

The CoGrothendieck construction #

Given a category 𝒮 and any pseudofunctor F from 𝒮ᵒᵖ to Cat, we associate to it a category ∫ᶜ F (TODO: promote CategoryStruct to Category instance), defined as follows:

The category ∫ᶜ F is equipped with a functor ∫ᶜ F ⥤ 𝒮 (TODO: define this functor), given by projecting to the first factors, i.e.

Naming conventions #

The name Grothendieck is reserved for the construction on covariant pseudofunctors from 𝒮 to Cat, whereas the word CoGrothendieck is used for the contravariant construction. This is consistent with the convention for the Grothendieck construction on 1-functors CategoryTheory.Grothendieck.

Future work / TODO #

  1. Once the bicategory of pseudofunctors has been defined, show that this construction forms a pseudofunctor from Pseudofunctor (LocallyDiscrete 𝒮) Catᵒᵖ to Cat.
  2. Deduce the results in CategoryTheory.Grothendieck as a specialization of Pseudofunctor.Grothendieck.
  3. Dualize all CoGrothendieck results to Grothendieck.

References #

[Vistoli2008] "Notes on Grothendieck Topologies, Fibered Categories and Descent Theory" by Angelo Vistoli

The type of objects in the fibered category associated to a pseudofunctor from a 1-category to Cat.

  • base : 𝒮

    The underlying object in the base category.

  • fiber : (F.obj { as := self.base })

    The object in the fiber of the base object.

Instances For
    theorem CategoryTheory.Pseudofunctor.Grothendieck.ext {𝒮 : Type u₁} {inst✝ : Category.{v₁, u₁} 𝒮} {F : Pseudofunctor (LocallyDiscrete 𝒮) Cat} {x y : F.Grothendieck} (base : x.base = y.base) (fiber : x.fiber y.fiber) :
    x = y

    Notation for the Grothendieck category associated to a pseudofunctor F.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      structure CategoryTheory.Pseudofunctor.Grothendieck.Hom {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮) Cat} (X Y : F.Grothendieck) :
      Type (max v₁ v₂)

      A morphism in the Grothendieck construction ∫ F between two points X Y : ∫ F consists of a morphism in the base category base : X.base ⟶ Y.base and a morphism in a fiber f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber.

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

        The type of objects in the fibered category associated to a contravariant pseudofunctor from a 1-category to Cat.

        • base : 𝒮

          The underlying object in the base category.

        • fiber : (F.obj { as := Opposite.op self.base })

          The object in the fiber of the base object.

        Instances For
          theorem CategoryTheory.Pseudofunctor.CoGrothendieck.ext {𝒮 : Type u₁} {inst✝ : Category.{v₁, u₁} 𝒮} {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {x y : F.CoGrothendieck} (base : x.base = y.base) (fiber : x.fiber y.fiber) :
          x = y

          Notation for the CoGrothendieck category associated to a pseudofunctor F.

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

            A morphism in the CoGrothendieck construction ∫ᶜ F between two points X Y : ∫ᶜ F consists of a morphism in the base category base : X.base ⟶ Y.base and a morphism in a fiber f.fiber : X.fiber ⟶ (F.map base.op.toLoc).obj Y.fiber.

            Instances For

              The projection ∫ᶜ F ⥤ 𝒮 given by projecting both objects and homs to the first factor.

              Equations
              Instances For
                @[simp]

                The CoGrothendieck construction is functorial: a strong natural transformation α : F ⟶ G induces a functor CoGrothendieck.map : ∫ᶜ F ⥤ ∫ᶜ G.

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

                  The natural isomorphism witnessing the pseudo-functoriality of CoGrothendieck.map.

                  Equations
                  Instances For