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 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 Y : CategoryTheory.Grothendieck F} (f g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber) : f = g

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 }

def CategoryTheory.Grothendieck.comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y 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_base {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).base = CategoryTheory.CategoryStruct.id X.base

@[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_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y Z : CategoryTheory.Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.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 Y 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 Y : CategoryTheory.Grothendieck F} {f g : X ⟶ Y} (h : f = g) : f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber

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

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.forget_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (x✝ x✝¹ : CategoryTheory.Grothendieck F) (f : x✝ ⟶ x✝¹) : (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.map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F 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.

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Grothendieck.map_obj_fiber {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F 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_obj_base {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.map α).obj X).base = X.base

theorem CategoryTheory.Grothendieck.map_obj {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {F 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 G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} {X 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 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 G 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 G 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.

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

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

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

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.

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

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

def CategoryTheory.Grothendieck.pre {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) : CategoryTheory.Functor (CategoryTheory.Grothendieck (G.comp F)) (CategoryTheory.Grothendieck F)

Applying a functor G : D ⥤ C to the base of the Grothendieck construction induces a functor Grothendieck (G ⋙ F) ⥤ Grothendieck F.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.pre_map_base {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp F)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.pre F G).map f).base = G.map f.base

@[simp]

theorem CategoryTheory.Grothendieck.pre_map_fiber {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) {X✝ Y✝ : CategoryTheory.Grothendieck (G.comp F)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.pre F G).map f).fiber = f.fiber

@[simp]

theorem CategoryTheory.Grothendieck.pre_obj_base {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) (X : CategoryTheory.Grothendieck (G.comp F)) : ((CategoryTheory.Grothendieck.pre F G).obj X).base = G.obj X.base

@[simp]

theorem CategoryTheory.Grothendieck.pre_obj_fiber {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (F : CategoryTheory.Functor C CategoryTheory.Cat) (G : CategoryTheory.Functor D C) (X : CategoryTheory.Grothendieck (G.comp F)) : ((CategoryTheory.Grothendieck.pre F G).obj X).fiber = X.fiber

def CategoryTheory.Grothendieck.ι {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C) : CategoryTheory.Functor (↑(F.obj c)) (CategoryTheory.Grothendieck F)

The inclusion of a fiber F.obj c of a functor F : C ⥤ Cat into its Grothendieck construction.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.ι_obj {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C) (d : ↑(F.obj c)) : (CategoryTheory.Grothendieck.ι F c).obj d = { base := c, fiber := d }

@[simp]

theorem CategoryTheory.Grothendieck.ι_map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C) {X✝ Y✝ : ↑(F.obj c)} (f : X✝ ⟶ Y✝) : (CategoryTheory.Grothendieck.ι F c).map f = { base := CategoryTheory.CategoryStruct.id ((fun (d : ↑(F.obj c)) => { base := c, fiber := d }) X✝).base, fiber := CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f }

instance CategoryTheory.Grothendieck.faithful_ι {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (c : C) : (CategoryTheory.Grothendieck.ι F c).Faithful

Equations

• ⋯ = ⋯

def CategoryTheory.Grothendieck.ιNatTrans {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C} (f : X ⟶ Y) : CategoryTheory.Grothendieck.ι F X ⟶ CategoryTheory.Functor.comp (F.map f) (CategoryTheory.Grothendieck.ι F Y)

Every morphism f : X ⟶ Y in the base category induces a natural transformation from the fiber inclusion ι F X to the composition F.map f ⋙ ι F Y.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.ιNatTrans_app_fiber {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C} (f : X ⟶ Y) (d : ↑(F.obj X)) : ((CategoryTheory.Grothendieck.ιNatTrans f).app d).fiber = CategoryTheory.CategoryStruct.id ((F.map f).obj ((CategoryTheory.Grothendieck.ι F X).obj d).fiber)

@[simp]

theorem CategoryTheory.Grothendieck.ιNatTrans_app_base {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : C} (f : X ⟶ Y) (d : ↑(F.obj X)) : ((CategoryTheory.Grothendieck.ιNatTrans f).app d).base = f

def CategoryTheory.Grothendieck.functorFrom {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_3} [CategoryTheory.Category.{u_7, u_3} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ CategoryTheory.Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (F.map f) (hom g)) (CategoryTheory.eqToHom ⋯))) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) E

Construct a functor from Grothendieck F to another category E by providing a family of functors on the fibers of Grothendieck F, a family of natural transformations on morphisms in the base of Grothendieck F and coherence data for this family of natural transformations.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.functorFrom_map {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_3} [CategoryTheory.Category.{u_7, u_3} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ CategoryTheory.Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (F.map f) (hom g)) (CategoryTheory.eqToHom ⋯))) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).map f = CategoryTheory.CategoryStruct.comp ((hom f.base).app X.fiber) ((fib Y.base).map f.fiber)

@[simp]

theorem CategoryTheory.Grothendieck.functorFrom_obj {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_3} [CategoryTheory.Category.{u_7, u_3} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ CategoryTheory.Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (F.map f) (hom g)) (CategoryTheory.eqToHom ⋯))) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).obj X = (fib X.base).obj X.fiber

def CategoryTheory.Grothendieck.ιCompFunctorFrom {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_3} [CategoryTheory.Category.{u_7, u_3} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ CategoryTheory.Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (F.map f) (hom g)) (CategoryTheory.eqToHom ⋯))) (c : C) : (CategoryTheory.Grothendieck.ι F c).comp (CategoryTheory.Grothendieck.functorFrom fib (fun {c c' : C} => hom) hom_id hom_comp) ≅ fib c

Grothendieck.ι F c composed with Grothendieck.functorFrom is isomorphic a functor on a fiber on F supplied as the first argument to Grothendieck.functorFrom.

Equations

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