Documentation

Mathlib.CategoryTheory.Bicategory.Grothendieck

The Grothendieck construction #

Given a category 𝒮 and any pseudofunctor F from 𝒮ᵒᵖ to Cat, we associate to it a category ∫ F, equipped with a functor ∫ F ⥤ 𝒮.

The category ∫ F is defined as follows:

The projection functor ∫ F ⥤ 𝒮 is then given by projecting to the first factors, i.e.

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 presheaf valued in types.

  • 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

    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

      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.

      Instances For

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

        Equations
        Instances For