mathlib documentation

category_theory.grothendieck

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 category_theory.functor.elements for the category of elements of functor F : C ⥤ Type.

@[nolint]
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 : (F.map 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 : (F.map base).obj X.fiber ⟶ Y.fiber.

@[ext]

The identity morphism in the Grothendieck category.

Equations

Composition of morphisms in the Grothendieck category.

Equations

The forgetful functor from grothendieck F to the source category.

Equations

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