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:

• Objects: pairs (S, a) where S is an object of the base category and a is an object of the category F(S).
• Morphisms: morphisms (R, b) ⟶ (S, a) are defined as pairs (f, h) where f : R ⟶ S is a morphism in 𝒮 and h : b ⟶ F(f)(a)

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

• On objects, it sends (S, a) to S
• On morphisms, it sends (f, h) to f

References

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

structure CategoryTheory.Pseudofunctor.Grothendieck {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) : Type (max u₁ u₂)

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.

theorem CategoryTheory.Pseudofunctor.Grothendieck.ext {𝒮 : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x y : F.Grothendieck}, x.base = y.base → HEq x.fiber y.fiber → x = y

def CategoryTheory.Pseudofunctor.Grothendieck.«term∫_» : Lean.ParserDescr

Notation for the Grothendieck category associated to a pseudofunctor F.

Equations

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

structure CategoryTheory.Pseudofunctor.Grothendieck.Hom {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.Grothendieck) (Y : F.Grothendieck) : Type (max v₁ v₂)

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 : X.fiber ⟶ (F.map self.base.op.toLoc).obj Y.fiber

  The morphism in the fiber over the domain.

instance CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} : CategoryTheory.CategoryStruct.{max v₂ v₁, max u₂ u₁} F.Grothendieck

Equations

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

@[simp]

theorem CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_base {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} : ∀ {x x_1 Z : F.Grothendieck} (f : x ⟶ x_1) (g : x_1 ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

@[simp]

theorem CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_fiber {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.Grothendieck) : (CategoryTheory.CategoryStruct.id X).fiber = (F.mapId { as := Opposite.op X.base }).inv.app X.fiber

@[simp]

theorem CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_id_base {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.Grothendieck) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base

@[simp]

theorem CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} : ∀ {x x_1 Z : F.Grothendieck} (f : x ⟶ x_1) (g : x_1 ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).fiber = CategoryTheory.CategoryStruct.comp f.fiber (CategoryTheory.CategoryStruct.comp ((F.map f.base.op.toLoc).map g.fiber) ((F.mapComp g.base.op.toLoc f.base.op.toLoc).inv.app Z.fiber))

@[simp]

theorem CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_Hom {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (X : F.Grothendieck) (Y : F.Grothendieck) : (X ⟶ Y) = X.Hom Y

theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a : F.Grothendieck} {b : F.Grothendieck} (f : a ⟶ b) (g : a ⟶ b) (hfg₁ : f.base = g.base) (hfg₂ : f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯)) : f = g

theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a : F.Grothendieck} {b : F.Grothendieck} (f : a ⟶ b) (g : a ⟶ b) : f = g ↔ ∃ (hfg : f.base = g.base), f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯)

theorem CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {a : F.Grothendieck} {b : F.Grothendieck} {f : a ⟶ b} {g : a ⟶ b} (h : f = g) : f.fiber = CategoryTheory.CategoryStruct.comp g.fiber (CategoryTheory.eqToHom ⋯)

instance CategoryTheory.Pseudofunctor.Grothendieck.category {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} : CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} F.Grothendieck

The category structure on ∫ F.

Equations

• CategoryTheory.Pseudofunctor.Grothendieck.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def CategoryTheory.Pseudofunctor.Grothendieck.forget {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) : CategoryTheory.Functor F.Grothendieck 𝒮

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

Equations

• CategoryTheory.Pseudofunctor.Grothendieck.forget F = { obj := fun (X : F.Grothendieck) => X.base, map := fun {X Y : F.Grothendieck} (f : X ⟶ Y) => f.base, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Pseudofunctor.Grothendieck.forget_map {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) : ∀ {X Y : F.Grothendieck} (f : X ⟶ Y), (CategoryTheory.Pseudofunctor.Grothendieck.forget F).map f = f.base

@[simp]

theorem CategoryTheory.Pseudofunctor.Grothendieck.forget_obj {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (X : F.Grothendieck) : (CategoryTheory.Pseudofunctor.Grothendieck.forget F).obj X = X.base