mathlib documentation


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 φ : ( β).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 ⟶ ( (op β)).obj f'.


See also category_theory.functor.elements for the category of elements of functor F : C ⥤ Type.

structure category_theory.grothendieck {C : Type u_1} [category_theory.category C] :
C category_theory.CatType (max u_1 u_6)

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

A morphism in the Grothendieck category F : C ⥤ Cat consists of base : X.base ⟶ Y.base and f.fiber : ( base).obj X.fiber ⟶ Y.fiber.


The identity morphism in the Grothendieck category.


Composition of morphisms in the Grothendieck category.


The forgetful functor from grothendieck F to the source category.


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.