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'

Grothendieck.functor makes the Grothendieck construction into a functor from the functor category C ⥤ Cat to the over category Over C in the category of categories.

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 ⋯

@[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 ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map g.base).map f.fiber) g.fiber)

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_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

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

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.map_map_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : ((CategoryTheory.Grothendieck.map α).map f).fiber = CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).app X.fiber) ((α.app Y.base).map f.fiber)

@[simp]

theorem CategoryTheory.Grothendieck.map_obj_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.map α).obj X).base = X.base

@[simp]

theorem CategoryTheory.Grothendieck.map_obj_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.map α).obj X).fiber = (α.app X.base).obj X.fiber

@[simp]

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

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

The Grothendieck construction is functorial: a natural transformation α : F ⟶ G induces a functor Grothendieck.map : Grothendieck F ⥤ Grothendieck G.

Equations

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

theorem CategoryTheory.Grothendieck.map_obj {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.map α).obj X = { base := X.base, fiber := (α.app X.base).obj X.fiber }

theorem CategoryTheory.Grothendieck.map_map {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} {X : CategoryTheory.Grothendieck F} {Y : CategoryTheory.Grothendieck F} {f : X ⟶ Y} : (CategoryTheory.Grothendieck.map α).map f = { base := f.base, fiber := CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).app X.fiber) ((α.app Y.base).map f.fiber) }

theorem CategoryTheory.Grothendieck.functor_comp_forget {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} : (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.forget G) = CategoryTheory.Grothendieck.forget F

The functor Grothendieck.map α : Grothendieck F ⥤ Grothendieck G lies over C.

theorem CategoryTheory.Grothendieck.map_id_eq {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (CategoryTheory.Grothendieck F))

def CategoryTheory.Grothendieck.mapIdIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.id F) ≅ CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (CategoryTheory.Grothendieck F))

Making the equality of functors into an isomorphism. Note: we should avoid equality of functors if possible, and we should prefer map_id_iso to map_id_eq whenever we can.

Equations

• CategoryTheory.Grothendieck.mapIdIso = CategoryTheory.eqToIso ⋯

theorem CategoryTheory.Grothendieck.map_comp_eq {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {G : CategoryTheory.Functor C CategoryTheory.Cat} {H : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) = (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.map β)

def CategoryTheory.Grothendieck.mapCompIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {G : CategoryTheory.Functor C CategoryTheory.Cat} {H : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) ≅ (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.map β)

Making the equality of functors into an isomorphism. Note: we should avoid equality of functors if possible, and we should prefer map_comp_iso to map_comp_eq whenever we can.

Equations

• CategoryTheory.Grothendieck.mapCompIso α β = CategoryTheory.eqToIso ⋯

def CategoryTheory.Grothendieck.functor {E : CategoryTheory.Cat} : CategoryTheory.Functor (CategoryTheory.Functor (↑E) CategoryTheory.Cat) (CategoryTheory.Over E)

The Grothendieck construction as a functor from the functor category E ⥤ Cat to the over category Over E.

Equations

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

@[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 Y : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X ⟶ Y), ↑((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).map f) = f.base

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

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 grothendieckTypeToCat, to speed up elaboration.

Equations

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

@[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_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_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 grothendieckTypeToCat, to speed up elaboration.

Equations

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

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