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] (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 : (F.map base).obj X.fiber ⟶ Y.fiber
Instances for category_theory.grothendieck
structure category_theory.grothendieck.hom {C : Type u_1} [category_theory.category C] {F : C category_theory.Cat} (X Y : category_theory.grothendieck F) :
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.

Instances for category_theory.grothendieck.hom
@[ext]
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.

Equations
def category_theory.grothendieck.comp {C : Type u_1} [category_theory.category C] {F : C category_theory.Cat} {X Y Z : category_theory.grothendieck F} (f : X.hom Y) (g : Y.hom Z) :
X.hom Z

Composition of morphisms in the Grothendieck category.

Equations

The forgetful functor from grothendieck F to the source category.

Equations
@[simp]

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

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