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

• https://stacks.math.columbia.edu/tag/02XV
• https://ncatlab.org/nlab/show/Grothendieck+construction

structure CategoryTheory.Grothendieck {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : Type (max u_1 u_4)

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

• base : C

  The underlying object in C

• fiber : ↑(F.obj self.base)

  The object in the fiber of the base object.

structure CategoryTheory.Grothendieck.Hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) (Y : CategoryTheory.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.

• base : X.base ⟶ Y.base

  The morphism between base objects.

• fiber : (F.map self.base).obj X.fiber ⟶ Y.fiber

  The morphism from the pushforward to the source fiber object to the target fiber object.

theorem CategoryTheory.Grothendieck.ext {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} (f : X.Hom Y) (g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber) : f = g

@[simp]

theorem CategoryTheory.Grothendieck.id_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : X.id.fiber = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.Grothendieck.id_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : X.id.base = CategoryTheory.CategoryStruct.id X.base

def CategoryTheory.Grothendieck.id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : X.Hom X

The identity morphism in the Grothendieck category.

Equations

• X.id = { base := CategoryTheory.CategoryStruct.id X.base, fiber := CategoryTheory.eqToHom ⋯ }

instance CategoryTheory.Grothendieck.instInhabitedHom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : Inhabited (X.Hom X)

Equations

• X.instInhabitedHom = { default := X.id }

@[simp]

theorem CategoryTheory.Grothendieck.comp_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} {Z : CategoryTheory.Grothendieck F} (f : X.Hom Y) (g : Y.Hom Z) : (CategoryTheory.Grothendieck.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

@[simp]

theorem CategoryTheory.Grothendieck.comp_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} {Z : CategoryTheory.Grothendieck F} (f : X.Hom Y) (g : Y.Hom Z) : (CategoryTheory.Grothendieck.comp f g).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map g.base).map f.fiber) g.fiber)

def CategoryTheory.Grothendieck.comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} {Z : CategoryTheory.Grothendieck F} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

Composition of morphisms in the Grothendieck category.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Grothendieck.instCategory {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : CategoryTheory.Category.{max u_5 u_3, max u_4 u_1} (CategoryTheory.Grothendieck F)

Equations

• CategoryTheory.Grothendieck.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Grothendieck.id_fiber' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.CategoryStruct.id X).fiber = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Grothendieck.congr {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} {f : X ⟶ Y} {g : X ⟶ Y} (h : f = g) : f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber

@[simp]

theorem CategoryTheory.Grothendieck.forget_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) (Y : CategoryTheory.Grothendieck F) (f : X ⟶ Y) : (CategoryTheory.Grothendieck.forget F).map f = f.base

@[simp]

theorem CategoryTheory.Grothendieck.forget_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.forget F).obj X = X.base

def CategoryTheory.Grothendieck.forget {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) C

The forgetful functor from Grothendieck F to the source category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_fst {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).fst = X.base

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_obj_snd {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) (Y : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) (f : X ⟶ Y) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).map f) = f.base

def CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Functor (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) G.Elements

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_map_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) : ∀ {X Y : G.Elements} (f : X ⟶ Y), ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).map f).base = ↑f

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_fiber_as {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).fiber.as = X.snd

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_obj_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).base = X.fst

def CategoryTheory.Grothendieck.grothendieckTypeToCatInverse {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Functor G.Elements (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat))

Auxiliary definition for grothendieck_Type_to_Cat, to speed up elaboration.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_fiber_as {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).fiber.as = X.snd

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).fst = X.base

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_obj_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.obj X).base = X.fst

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).base = CategoryTheory.CategoryStruct.id X.base

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_hom_app_coe {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.hom.app X) = CategoryTheory.CategoryStruct.id X.fst

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_counitIso_inv_app_coe {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).counitIso.inv.app X) = CategoryTheory.CategoryStruct.id X.fst

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) : ∀ {X Y : G.Elements} (f : X ⟶ Y), ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).inverse.map f).base = ↑f

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).fiber = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).fiber = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) (Y : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) (f : X ⟶ Y) : ↑((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.map f) = f.base

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).snd = X.fiber.as

@[simp]

theorem CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).base = CategoryTheory.CategoryStruct.id X.base

def CategoryTheory.Grothendieck.grothendieckTypeToCat {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat) ≌ 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

• One or more equations did not get rendered due to their size.