Documentation

Mathlib.CategoryTheory.FiberedCategory.Grothendieck

The Grothendieck construction gives a fibered category #

In this file we show that the Grothendieck construction 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.CoGrothendieck.domainCartesianLift {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) :
F.CoGrothendieck

The domain of the Cartesian lift of f.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift {𝒮 : Type u_1} [Category.{v_1, 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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance CategoryTheory.Pseudofunctor.CoGrothendieck.isHomLift_cartesianLift {𝒮 : Type u_1} [Category.{v_1, 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.CoGrothendieck.homCartesianLift {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} {a : ↑(F.obj { as := Opposite.op S })} (f : R ⟶ S) {a' : F.CoGrothendieck} (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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance CategoryTheory.Pseudofunctor.CoGrothendieck.isHomLift_homCartesianLift {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {R S : 𝒮} (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S) {a' : F.CoGrothendieck} {φ' : 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.CoGrothendieck.isStronglyCartesian_homCartesianLift {𝒮 : Type u_1} [Category.{v_1, 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.CoGrothendieck.instIsFiberedForget {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} :
        (forget F).IsFibered

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

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

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber {𝒮 : Type u_1} [Category.{v_1, 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.toNatTrans.app b)
          source
          @[simp]
          theorem CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_base {𝒮 : Type u_1} [Category.{v_1, 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.CoGrothendieck.ι_obj_fiber {𝒮 : Type u_1} [Category.{v_1, 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.CoGrothendieck.ι_obj_base {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) (a : ↑(F.obj { as := Opposite.op S })) :
          ((ι F S).obj a).base = S
          source
          def CategoryTheory.Pseudofunctor.CoGrothendieck.compIso {𝒮 : Type u_1} [Category.{v_1, 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.CoGrothendieck.compIso_inv_app {𝒮 : Type u_1} [Category.{v_1, 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.CoGrothendieck.compIso_hom_app {𝒮 : Type u_1} [Category.{v_1, 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.CoGrothendieck.comp_const {𝒮 : Type u_1} [Category.{v_1, 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.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
            (Functor.Fiber.inducedFunctor ⋯).Full
            source
            instance CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
            (Functor.Fiber.inducedFunctor ⋯).Faithful
            source
            instance CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
            (Functor.Fiber.inducedFunctor ⋯).EssSurj
            source
            instance CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) (S : 𝒮) :
            (Functor.Fiber.inducedFunctor ⋯).IsEquivalence
            source
            @[instance_reducible]
            noncomputable instance CategoryTheory.Pseudofunctor.CoGrothendieck.instHasFibersForget {𝒮 : Type u_1} [Category.{v_1, u_1} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) :
            HasFibers (forget F)

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

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