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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : Type (max u u₂)

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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X Y : CategoryTheory.Grothendieck F) : Type (max v v₂)

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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : CategoryTheory.Category.{max v₂ v, max u₂ u} (CategoryTheory.Grothendieck F)

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.id_base {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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_obj_fiber {C : Type u} [CategoryTheory.Category.{v, u} 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_map_fiber {C : Type u} [CategoryTheory.Category.{v, u} 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_base {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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.compAsSmallFunctorEquivalenceInverse {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor))

The inverse functor to build the equivalence compAsSmallFunctorEquivalence.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_base {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).obj X).base = X.base

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_obj_fiber {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck F) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).obj X).fiber = CategoryTheory.AsSmall.up.obj X.fiber

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).map f).fiber = CategoryTheory.AsSmall.up.map f.fiber

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).map f).base = f.base

def CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Functor (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)) (CategoryTheory.Grothendieck F)

The functor to build the equivalence compAsSmallFunctorEquivalence.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).map f).base = f.base

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_fiber {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).obj X).fiber = CategoryTheory.AsSmall.down.obj X.fiber

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_obj_base {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (X : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).obj X).base = X.base

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {X✝ Y✝ : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).map f).fiber = CategoryTheory.AsSmall.down.map f.fiber

def CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor) ≌ CategoryTheory.Grothendieck F

Taking the Grothendieck construction on F ⋙ asSmallFunctor, where asSmallFunctor : Cat ⥤ Cat is the functor which turns each category into a small category of a (potentiall) larger universe, is equivalent to the Grothendieck construction on F itself.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).comp (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F))

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).functor = CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)))

@[simp]

theorem CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).inverse = CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F

def CategoryTheory.Grothendieck.mapWhiskerRightAsSmallFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) {G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) : CategoryTheory.Grothendieck.map (CategoryTheory.whiskerRight α CategoryTheory.Cat.asSmallFunctor) ≅ (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).functor.comp ((CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence G).inverse)

Mapping a Grothendieck construction along the whiskering of any natural transformation α : F ⟶ G with the functor asSmallFunctor : Cat ⥤ Cat is naturally isomorphic to conjugating map α with the equivalence between Grothendieck (F ⋙ asSmallFunctor) and Grothendieck F.

Equations

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

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} [CategoryTheory.Category.{v, u} 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_fst {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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_snd {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as

def CategoryTheory.Grothendieck.grothendieckTypeToCatInverse {C : Type u} [CategoryTheory.Category.{v, u} 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_fiber_as {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : G.Elements) : ((CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G).obj X).base = X.fst

def CategoryTheory.Grothendieck.grothendieckTypeToCat {C : Type u} [CategoryTheory.Category.{v, u} 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_counitIso_inv_app_coe {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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_inv_app_fiber {C : Type u} [CategoryTheory.Category.{v, u} 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_hom_app_coe {C : Type u} [CategoryTheory.Category.{v, u} 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_functor_map_coe {C : Type u} [CategoryTheory.Category.{v, u} 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_inverse_obj_base {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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_hom_app_base {C : Type u} [CategoryTheory.Category.{v, u} 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_inv_app_base {C : Type u} [CategoryTheory.Category.{v, u} 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_inverse_map_base {C : Type u} [CategoryTheory.Category.{v, u} 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_functor_obj_fst {C : Type u} [CategoryTheory.Category.{v, u} 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_functor_obj_snd {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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_obj_base {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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_map_fiber {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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_fiber {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (c : C) : (CategoryTheory.Grothendieck.ι F c).Faithful

def CategoryTheory.Grothendieck.ιNatTrans {C : Type u} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} 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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} 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.