# The Grothendieck construction #

Given a functor F : C ⥤ Cat, the objects of Grothendieck F consist of dependent pairs (b, f), where b : C and f : F.obj c, and a morphism (b, f) ⟶ (b', f') is a pair β : b ⟶ b' in C, and φ : (F.map β).obj f ⟶ f'

Categories such as PresheafedSpace are in fact examples of this construction, and it may be interesting to try to generalize some of the development there.

## Implementation notes #

Really we should treat Cat as a 2-category, and allow F to be a 2-functor.

There is also a closely related construction starting with G : Cᵒᵖ ⥤ Cat, where morphisms consists again of β : b ⟶ b' and φ : f ⟶ (F.map (op β)).obj f'.

## References #

See also CategoryTheory.Functor.Elements for the category of elements of functor F : C ⥤ Type.

• https://stacks.math.columbia.edu/tag/02XV
• https://ncatlab.org/nlab/show/Grothendieck+construction
structure CategoryTheory.Grothendieck {C : Type u_1} [] :
Type (max u_1 u_4)

The Grothendieck construction (often written as ∫ F in mathematics) for a functor F : C ⥤ Cat gives a category whose

• objects X consist of X.base : C and X.fiber : F.obj base
• morphisms f : X ⟶ Y consist of base : X.base ⟶ Y.base and f.fiber : (F.map base).obj X.fiber ⟶ Y.fiber
• base : C

The underlying object in C

• fiber : (F.obj self.base)

The object in the fiber of the base object.

Instances For
structure CategoryTheory.Grothendieck.Hom {C : Type u_1} [] (X : ) (Y : ) :
Type (max u_3 u_5)

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

The morphism from the pushforward to the source fiber object to the target fiber object.

Instances For
theorem CategoryTheory.Grothendieck.ext {C : Type u_1} [] {X : } {Y : } (f : X.Hom Y) (g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : = g.fiber) :
f = g
@[simp]
theorem CategoryTheory.Grothendieck.id_fiber {C : Type u_1} [] (X : ) :
X.id.fiber =
@[simp]
theorem CategoryTheory.Grothendieck.id_base {C : Type u_1} [] (X : ) :
X.id.base =
def CategoryTheory.Grothendieck.id {C : Type u_1} [] (X : ) :
X.Hom X

The identity morphism in the Grothendieck category.

Equations
• X.id = { base := , fiber := }
Instances For
instance CategoryTheory.Grothendieck.instInhabitedHom {C : Type u_1} [] (X : ) :
Inhabited (X.Hom X)
Equations
• X.instInhabitedHom = { default := X.id }
@[simp]
theorem CategoryTheory.Grothendieck.comp_base {C : Type u_1} [] {X : } {Y : } {Z : } (f : X.Hom Y) (g : Y.Hom Z) :
@[simp]
theorem CategoryTheory.Grothendieck.comp_fiber {C : Type u_1} [] {X : } {Y : } {Z : } (f : X.Hom Y) (g : Y.Hom Z) :
.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((F.map g.base).map f.fiber) g.fiber)
def CategoryTheory.Grothendieck.comp {C : Type u_1} [] {X : } {Y : } {Z : } (f : X.Hom Y) (g : Y.Hom Z) :
X.Hom Z

Composition of morphisms in the Grothendieck category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.Grothendieck.instCategory =
@[simp]
theorem CategoryTheory.Grothendieck.id_fiber' {C : Type u_1} [] (X : ) :
theorem CategoryTheory.Grothendieck.congr {C : Type u_1} [] {X : } {Y : } {f : X Y} {g : X Y} (h : f = g) :
f.fiber =
@[simp]
theorem CategoryTheory.Grothendieck.forget_map {C : Type u_1} [] (X : ) (Y : ) (f : X Y) :
f = f.base
@[simp]
theorem CategoryTheory.Grothendieck.forget_obj {C : Type u_1} [] (X : ) :
X = X.base

The forgetful functor from Grothendieck F to the source category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_fst {C : Type u_1} [] (G : ) (X : ) :
.fst = X.base
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd {C : Type u_1} [] (G : ) (X : ) :
.snd = X.fiber.as
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe {C : Type u_1} [] (G : ) (X : ) (Y : ) (f : X Y) :
= f.base

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_map_base {C : Type u_1} [] (G : ) :
∀ {X Y : G.Elements} (f : X Y), .base = f
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as {C : Type u_1} [] (G : ) (X : G.Elements) :
.fiber.as = X.snd
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_base {C : Type u_1} [] (G : ) (X : G.Elements) :
.base = X.fst

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as {C : Type u_1} [] (G : ) (X : G.Elements) :
(.obj X).fiber.as = X.snd
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst {C : Type u_1} [] (G : ) (X : ) :
(.obj X).fst = X.base
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base {C : Type u_1} [] (G : ) (X : G.Elements) :
(.obj X).base = X.fst
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base {C : Type u_1} [] (G : ) (X : ) :
(.hom.app X).base =
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe {C : Type u_1} [] (G : ) (X : G.Elements) :
(.counitIso.hom.app X) =
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe {C : Type u_1} [] (G : ) (X : G.Elements) :
(.counitIso.inv.app X) =
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base {C : Type u_1} [] (G : ) :
∀ {X Y : G.Elements} (f : X Y), (.map f).base = f
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber {C : Type u_1} [] (G : ) (X : ) :
(.inv.app X).fiber =
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber {C : Type u_1} [] (G : ) (X : ) :
(.hom.app X).fiber =
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe {C : Type u_1} [] (G : ) (X : ) (Y : ) (f : X Y) :
(.map f) = f.base
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd {C : Type u_1} [] (G : ) (X : ) :
(.obj X).snd = X.fiber.as
@[simp]
theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base {C : Type u_1} [] (G : ) (X : ) :
(.inv.app X).base =
def CategoryTheory.Grothendieck.grothendieckTypeToCat {C : Type u_1} [] (G : ) :
G.Elements

The Grothendieck construction applied to a functor to Type (thought of as a functor to Cat by realising a type as a discrete category) is the same as the 'category of elements' construction.

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