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.

source
@[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
source
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.

source
@[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

source
@[simp]
theorem category_theory.grothendieck.id_fiber {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :
X.id.fiber = category_theory.eq_to_hom _

source
def category_theory.grothendieck.id {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :
X.hom X

The identity morphism in the Grothendieck category.

Equations
source
@[simp]
theorem category_theory.grothendieck.id_base {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :
X.id.base = 𝟙 X.base

source
@[instance]
def category_theory.grothendieck.inhabited {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :
inhabited (X.hom X)

Equations
source
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
source
@[simp]
theorem category_theory.grothendieck.comp_base {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) :
(category_theory.grothendieck.comp f g).base = f.base ≫ g.base

source
@[simp]
theorem category_theory.grothendieck.comp_fiber {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) :
(category_theory.grothendieck.comp f g).fiber = category_theory.eq_to_hom _ ≫ (F.map g.base).map f.fiber ≫ g.fiber

source
@[instance]
def category_theory.grothendieck.category_theory.category {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} :
category_theory.category (category_theory.grothendieck F)

Equations
source
@[simp]
theorem category_theory.grothendieck.id_fiber' {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} (X : category_theory.grothendieck F) :
(𝟙 X).fiber = category_theory.eq_to_hom _

source
theorem category_theory.grothendieck.congr {C : Type u_1} [category_theory.category C] {F : C ⥤ category_theory.Cat} {X Y : category_theory.grothendieck F} {f g : X ⟶ Y} (h : f = g) :
f.fiber = category_theory.eq_to_hom _ ≫ g.fiber

source
@[simp]
theorem category_theory.grothendieck.forget_map {C : Type u_1} [category_theory.category C] (F : C ⥤ category_theory.Cat) (X Y : category_theory.grothendieck F) (f : X ⟶ Y) :
(category_theory.grothendieck.forget F).map f = f.base

source
@[simp]
theorem category_theory.grothendieck.forget_obj {C : Type u_1} [category_theory.category C] (F : C ⥤ category_theory.Cat) (X : category_theory.grothendieck F) :
(category_theory.grothendieck.forget F).obj X = X.base

source
def category_theory.grothendieck.forget {C : Type u_1} [category_theory.category C] (F : C ⥤ category_theory.Cat) :
category_theory.grothendieck F ⥤ C

The forgetful functor from grothendieck F to the source category.

Equations
source
def category_theory.grothendieck.grothendieck_Type_to_Cat {C : Type u_1} [category_theory.category C] (G : C ⥤ Type w) :
category_theory.grothendieck (G ⋙ category_theory.Type_to_Cat) ≌ 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