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

Naming conventions

The name Grothendieck is reserved for the construction on covariant pseudofunctors from 𝒮 to Cat, whereas the word CoGrothendieck will be 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. Develop the covariant version of CoGrothendieck and deduce the results in CategoryTheory.Grothendieck as a specialization of the results in this file.

References

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

structure CategoryTheory.Pseudofunctor.CoGrothendieck {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) 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.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

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

def CategoryTheory.Pseudofunctor.CoGrothendieck.«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.CoGrothendieck.Hom {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (X Y : F.CoGrothendieck) : Type (max v₁ v₂)

A morphism in the Grothendieck category consists of base : X.base ⟶ Y.base and f.fiber : X.fiber ⟶ (F.map base.op.toLoc).obj 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.CoGrothendieck.categoryStruct {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} : CategoryStruct.{max v₂ v₁, max u₂ u₁} F.CoGrothendieck

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {x✝ x✝¹ Z : F.CoGrothendieck} (f : x✝.Hom x✝¹) (g : x✝¹.Hom Z) : (CategoryStruct.comp f g).fiber = CategoryStruct.comp f.fiber (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))

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

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

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

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

The category structure on ∫ᶜ F.

Equations

• CategoryTheory.Pseudofunctor.CoGrothendieck.category = { toCategoryStruct := CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

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

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

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.Pseudofunctor.CoGrothendieck.map {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F G : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (α : F ⟶ G) : Functor F.CoGrothendieck G.CoGrothendieck

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

Equations

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

@[simp]

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F G : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (α : F ⟶ G) (a : F.CoGrothendieck) : ((map α).obj a).fiber = (α.app { as := Opposite.op a.base }).obj a.fiber

@[simp]

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F G : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (α : F ⟶ G) {a b : F.CoGrothendieck} (f : a ⟶ b) : ((map α).map f).fiber = CategoryStruct.comp ((α.app { as := Opposite.op a.base }).map f.fiber) ((α.naturality f.base.op.toLoc).hom.app b.fiber)

@[simp]

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_base {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F G : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (α : F ⟶ G) (a : F.CoGrothendieck) : ((map α).obj a).base = a.base

@[simp]

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_base {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F G : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (α : F ⟶ G) {a b : F.CoGrothendieck} (f : a ⟶ b) : ((map α).map f).base = f.base

@[simp]

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.map_id_map {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} {x y : F.CoGrothendieck} (f : x ⟶ y) : (map (CategoryStruct.id F)).map f = f

@[simp]

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.map_comp_forget {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F G : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (α : F ⟶ G) : (map α).comp (forget G) = forget F

def CategoryTheory.Pseudofunctor.CoGrothendieck.mapIdIso {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) : map (CategoryStruct.id F) ≅ Functor.id F.CoGrothendieck

The natural isomorphism witnessing the pseudo-unity constraint of Grothendieck.map.

Equations

• CategoryTheory.Pseudofunctor.CoGrothendieck.mapIdIso F = CategoryTheory.NatIso.ofComponents (fun (x : F.CoGrothendieck) => CategoryTheory.eqToIso ⋯) ⋯

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.map_id_eq {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] (F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat) : map (CategoryStruct.id F) = Functor.id F.CoGrothendieck

def CategoryTheory.Pseudofunctor.CoGrothendieck.mapCompIso {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F G H : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (α : F ⟶ G) (β : G ⟶ H) : map (CategoryStruct.comp α β) ≅ (map α).comp (map β)

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

Equations

• CategoryTheory.Pseudofunctor.CoGrothendieck.mapCompIso α β = CategoryTheory.NatIso.ofComponents (fun (x : F.CoGrothendieck) => CategoryTheory.eqToIso ⋯) ⋯

theorem CategoryTheory.Pseudofunctor.CoGrothendieck.map_comp_eq {𝒮 : Type u₁} [Category.{v₁, u₁} 𝒮] {F G H : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat} (α : F ⟶ G) (β : G ⟶ H) : map (CategoryStruct.comp α β) = (map α).comp (map β)