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'.

References #

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] (F : C category_theory.Cat) :
Type (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
Instances for category_theory.grothendieck

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.

Instances for category_theory.grothendieck.hom
theorem category_theory.grothendieck.ext {C : Type u_1} [category_theory.category C] {F : C category_theory.Cat} {X Y : category_theory.grothendieck F} (f g : X.hom Y) (w_base : f.base = g.base) (w_fiber : category_theory.eq_to_hom _ f.fiber = g.fiber) :
f = g

The identity morphism in the Grothendieck category.


Composition of morphisms in the Grothendieck category.


The forgetful functor from grothendieck F to the source category.


Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.


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.