Documentation

Mathlib.CategoryTheory.FiberedCategory.Grothendieck

The Grothendieck construction gives a fibered category #

In this file we show that the Grothendieck applied to a pseudofunctor F gives a fibered category over the base category.

We also provide a HasFibers instance to ∫ F, such that the fiber over S is the category F(S).

References #

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

source
@[reducible, inline]
abbrev CategoryTheory.Pseudofunctor.Grothendieck.domainCartesianLift {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) :
F.Grothendieck

The domain of the cartesian lift of f.

Equations
    Instances For
      source
      @[reducible, inline]
      abbrev CategoryTheory.Pseudofunctor.Grothendieck.cartesianLift {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) :
      domainCartesianLift a f ⟶ { base := S, fiber := a }

      The cartesian lift of f.

      Equations
        Instances For
          source
          instance CategoryTheory.Pseudofunctor.Grothendieck.isHomLift_cartesianLift {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) :
          (forget F).IsHomLift f (cartesianLift a f)
          source
          @[reducible, inline]
          abbrev CategoryTheory.Pseudofunctor.Grothendieck.homCartesianLift {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} {a : ↑(F.obj { as := Opposite.op S })} (f : R ⟶ S) {a' : F.Grothendieck} (g : a'.base ⟶ R) (φ' : a' ⟶ { base := S, fiber := a }) [(forget F).IsHomLift (CategoryStruct.comp g f) φ'] :
          a' ⟶ domainCartesianLift a f

          Given some lift φ' of g ≫ f, the canonical map from the domain of φ' to the domain of the cartesian lift of f.

          Equations
            Instances For
              source
              instance CategoryTheory.Pseudofunctor.Grothendieck.isHomLift_homCartesianLift {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) {a' : F.Grothendieck} {φ' : a' ⟶ { base := S, fiber := a }} {g : a'.base ⟶ R} [(forget F).IsHomLift (CategoryStruct.comp g f) φ'] :
              (forget F).IsHomLift g (homCartesianLift f g φ')
              source
              theorem CategoryTheory.Pseudofunctor.Grothendieck.isStronglyCartesian_homCartesianLift {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) :
              (forget F).IsStronglyCartesian f (cartesianLift a f)
              source
              instance CategoryTheory.Pseudofunctor.Grothendieck.instIsFiberedForget {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} :
              (forget F).IsFibered

              forget F : ∫ F ⥤ 𝒮 is a fibered category.

              source
              def CategoryTheory.Pseudofunctor.Grothendieck.ι {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
              Functor (↑(F.obj { as := Opposite.op S })) F.Grothendieck

              The inclusion map from F(S) into ∫ F.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.Grothendieck.ι_obj_fiber {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) (a : ↑(F.obj { as := Opposite.op S })) :
                  ((ι F S).obj a).fiber = a
                  source
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.Grothendieck.ι_map_base {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) {a b : ↑(F.obj { as := Opposite.op S })} (φ : a ⟶ b) :
                  ((ι F S).map φ).base = CategoryStruct.id S
                  source
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.Grothendieck.ι_map_fiber {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) {a b : ↑(F.obj { as := Opposite.op S })} (φ : a ⟶ b) :
                  ((ι F S).map φ).fiber = CategoryStruct.comp φ ((F.mapId { as := Opposite.op S }).inv.app b)
                  source
                  @[simp]
                  theorem CategoryTheory.Pseudofunctor.Grothendieck.ι_obj_base {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) (a : ↑(F.obj { as := Opposite.op S })) :
                  ((ι F S).obj a).base = S
                  source
                  def CategoryTheory.Pseudofunctor.Grothendieck.compIso {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
                  (ι F S).comp (forget F) ≅ (Functor.const ↑(F.obj { as := Opposite.op S })).obj S

                  The natural isomorphism encoding comp_const.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Pseudofunctor.Grothendieck.compIso_inv_app {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) (X : ↑(F.obj { as := Opposite.op S })) :
                      (compIso F S).inv.app X = CategoryStruct.id S
                      source
                      @[simp]
                      theorem CategoryTheory.Pseudofunctor.Grothendieck.compIso_hom_app {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) (X : ↑(F.obj { as := Opposite.op S })) :
                      (compIso F S).hom.app X = CategoryStruct.id S
                      source
                      theorem CategoryTheory.Pseudofunctor.Grothendieck.comp_const {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
                      (ι F S).comp (forget F) = (Functor.const ↑(F.obj { as := Opposite.op S })).obj S
                      source
                      instance CategoryTheory.Pseudofunctor.Grothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor {𝒮 : Type u_1} [Category.{u_3, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
                      (Functor.Fiber.inducedFunctor ⋯).Full
                      source
                      instance CategoryTheory.Pseudofunctor.Grothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor {𝒮 : Type u_1} [Category.{u_3, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
                      (Functor.Fiber.inducedFunctor ⋯).Faithful
                      source
                      instance CategoryTheory.Pseudofunctor.Grothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor {𝒮 : Type u_1} [Category.{u_3, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
                      (Functor.Fiber.inducedFunctor ⋯).EssSurj
                      source
                      instance CategoryTheory.Pseudofunctor.Grothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor {𝒮 : Type u_1} [Category.{u_3, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
                      (Functor.Fiber.inducedFunctor ⋯).IsEquivalence
                      source
                      noncomputable instance CategoryTheory.Pseudofunctor.Grothendieck.instHasFibersForget {𝒮 : Type u_1} [Category.{u_2, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) :
                      HasFibers (forget F)

                      HasFibers instance for ∫ F, where the fiber over S is F.obj ⟨op S⟩.

                      Equations