The Grothendieck and CoGrothendieck constructions #
The Grothendieck construction #
Given a category 𝒮 and any pseudofunctor F from 𝒮 to Cat, we associate to it a category
∫ F, defined as follows:
- Objects: pairs
(S, a)whereSis an object of the base category andais an object of the categoryF(S). - Morphisms: morphisms
(R, b) ⟶ (S, a)are defined as pairs(f, h)wheref : R ⟶ Sis a morphism in𝒮andh : F(f)(a) ⟶ b
The category ∫ F is equipped with a projection functor ∫ F ⥤ 𝒮,
given by projecting to the first factors, i.e.
- On objects, it sends
(S, a)toS - On morphisms, it sends
(f, h)tof
The CoGrothendieck construction #
Given a category 𝒮 and any pseudofunctor F from 𝒮ᵒᵖ to Cat, we associate to it a category
∫ᶜ F (TODO: promote CategoryStruct to Category instance), defined as follows:
- Objects: pairs
(S, a)whereSis an object of the base category andais an object of the categoryF(S). - Morphisms: morphisms
(R, b) ⟶ (S, a)are defined as pairs(f, h)wheref : R ⟶ Sis a morphism in𝒮andh : b ⟶ F(f)(a)
The category ∫ᶜ F is equipped with a functor ∫ᶜ F ⥤ 𝒮 (TODO: define this functor),
given by projecting to the first factors, i.e.
- On objects, it sends
(S, a)toS - On morphisms, it sends
(f, h)tof
Naming conventions #
The name Grothendieck is reserved for the construction on covariant pseudofunctors from 𝒮 to
Cat, whereas the word CoGrothendieck is used for the contravariant construction.
This is consistent with the convention for the Grothendieck construction on 1-functors
CategoryTheory.Grothendieck.
Future work / TODO #
- Once the bicategory of pseudofunctors has been defined, show that this construction forms a
pseudofunctor from
Pseudofunctor (LocallyDiscrete 𝒮) CatᵒᵖtoCat. - Deduce the results in
CategoryTheory.Grothendieckas a specialization ofPseudofunctor.Grothendieck. - Dualize all
CoGrothendieckresults toGrothendieck.
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 pseudofunctor from a 1-category to Cat.
- base : 𝒮
The underlying object in the base category.
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 construction ∫ F between two points X Y : ∫ F consists of
a morphism in the base category base : X.base ⟶ Y.base and
a morphism in a fiber f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber.
The morphism between base objects.
The morphism in the fiber over the domain.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- X.instInhabitedHom = { default := CategoryTheory.CategoryStruct.id X }
The type of objects in the fibered category associated to a contravariant pseudofunctor from a 1-category to Cat.
- 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 CoGrothendieck 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 CoGrothendieck construction ∫ᶜ F between two points X Y : ∫ᶜ F consists of
a morphism in the base category base : X.base ⟶ Y.base and
a morphism in a fiber f.fiber : X.fiber ⟶ (F.map base.op.toLoc).obj Y.fiber.
The morphism between base objects.
The morphism in the fiber over the domain.
Instances For
Equations
- One or more equations did not get rendered due to their size.
The category structure on ∫ᶜ F.
Equations
- CategoryTheory.Pseudofunctor.CoGrothendieck.category = { toCategoryStruct := CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
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 := ⋯ }
Instances For
The CoGrothendieck construction is functorial: a strong natural transformation α : F ⟶ G
induces a functor CoGrothendieck.map : ∫ᶜ F ⥤ ∫ᶜ G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural isomorphism witnessing the pseudo-unity constraint of CoGrothendieck.map.
Equations
Instances For
The natural isomorphism witnessing the pseudo-functoriality of CoGrothendieck.map.