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

Notable constructions

• Grothendieck F is the Grothendieck construction.
• Elements of Grothendieck F whose base is c : C can be transported along f : c ⟶ d using transport.
• A natural transformation α : F ⟶ G induces map α : Grothendieck F ⥤ Grothendieck G.
• The Grothendieck construction and map together form a functor (functor) from the functor category E ⥤ Cat to the over category Over E.
• A functor G : D ⥤ C induces pre F G : Grothendieck (G ⋙ F) ⥤ Grothendieck 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} [Category.{v, u} C] (F : Functor C 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} [Category.{v, u} C] {F : Functor C Cat} (X Y : 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} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (f g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : CategoryStruct.comp (eqToHom ⋯) f.fiber = g.fiber) : f = g

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Grothendieck.base_eqToHom {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (h : X = Y) : (eqToHom h).base = eqToHom ⋯

@[simp]

theorem CategoryTheory.Grothendieck.fiber_eqToHom {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (h : X = Y) : (eqToHom h).fiber = eqToHom ⋯

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

def CategoryTheory.Grothendieck.transport {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : Grothendieck F

If F : C ⥤ Cat is a functor and t : c ⟶ d is a morphism in C, then transport maps each c-based element of Grothendieck F to a d-based element.

Equations

• x.transport t = { base := c, fiber := (F.map t).obj x.fiber }

@[simp]

theorem CategoryTheory.Grothendieck.transport_fiber {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.transport t).fiber = (F.map t).obj x.fiber

@[simp]

theorem CategoryTheory.Grothendieck.transport_base {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.transport t).base = c

def CategoryTheory.Grothendieck.toTransport {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : x ⟶ x.transport t

If F : C ⥤ Cat is a functor and t : c ⟶ d is a morphism in C, then transport maps each c-based element x of Grothendieck F to a d-based element x.transport t.

toTransport is the morphism x ⟶ x.transport t induced by t and the identity on fibers.

Equations

• x.toTransport t = { base := t, fiber := CategoryTheory.CategoryStruct.id ((F.map t).obj x.fiber) }

@[simp]

theorem CategoryTheory.Grothendieck.toTransport_fiber {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.toTransport t).fiber = CategoryStruct.id ((F.map t).obj x.fiber)

@[simp]

theorem CategoryTheory.Grothendieck.toTransport_base {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (t : x.base ⟶ c) : (x.toTransport t).base = t

def CategoryTheory.Grothendieck.isoMk {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).obj X.fiber ≅ Y.fiber) : X ≅ Y

Construct an isomorphism in a Grothendieck construction from isomorphisms in its base and fiber.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.isoMk_inv_base {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).obj X.fiber ≅ Y.fiber) : (isoMk e₁ e₂).inv.base = e₁.inv

@[simp]

theorem CategoryTheory.Grothendieck.isoMk_hom_fiber {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).obj X.fiber ≅ Y.fiber) : (isoMk e₁ e₂).hom.fiber = e₂.hom

@[simp]

theorem CategoryTheory.Grothendieck.isoMk_inv_fiber {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).obj X.fiber ≅ Y.fiber) : (isoMk e₁ e₂).inv.fiber = CategoryStruct.comp ((F.map e₁.inv).map e₂.inv) (eqToHom ⋯)

@[simp]

theorem CategoryTheory.Grothendieck.isoMk_hom_base {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).obj X.fiber ≅ Y.fiber) : (isoMk e₁ e₂).hom.base = e₁.hom

def CategoryTheory.Grothendieck.transportIso {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (α : x.base ≅ c) : x.transport α.hom ≅ x

If F : C ⥤ Cat and x : Grothendieck F, then every C-isomorphism α : x.base ≅ c induces an isomorphism between x and its transport along α

Equations

• x.transportIso α = (CategoryTheory.Grothendieck.isoMk α (CategoryTheory.Iso.refl ((F.map α.hom).obj x.fiber))).symm

@[simp]

theorem CategoryTheory.Grothendieck.transportIso_inv_base {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).inv.base = α.hom

@[simp]

theorem CategoryTheory.Grothendieck.transportIso_hom_base {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).hom.base = α.inv

@[simp]

theorem CategoryTheory.Grothendieck.transportIso_inv_fiber {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).inv.fiber = CategoryStruct.id ((F.map α.hom).obj x.fiber)

@[simp]

theorem CategoryTheory.Grothendieck.transportIso_hom_fiber {C : Type u} [Category.{v, u} C] {F : Functor C Cat} (x : Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).hom.fiber = eqToHom ⋯

def CategoryTheory.Grothendieck.forget {C : Type u} [Category.{v, u} C] (F : Functor C Cat) : Functor (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} [Category.{v, u} C] (F : Functor C Cat) {X✝ Y✝ : Grothendieck F} (f : X✝ ⟶ Y✝) : (forget F).map f = f.base

@[simp]

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

def CategoryTheory.Grothendieck.map {C : Type u} [Category.{v, u} C] {F G : Functor C Cat} (α : F ⟶ G) : Functor (Grothendieck F) (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} [Category.{v, u} C] {F G : Functor C Cat} (α : F ⟶ G) {X Y : Grothendieck F} (f : X ⟶ Y) : ((map α).map f).base = f.base

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

• CategoryTheory.Grothendieck.mapIdIso = CategoryTheory.eqToIso ⋯

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

def CategoryTheory.Grothendieck.mapCompIso {C : Type u} [Category.{v, u} C] {F G H : Functor C Cat} (α : F ⟶ G) (β : G ⟶ H) : map (CategoryStruct.comp α β) ≅ (map α).comp (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} [Category.{v, u} C] (F : Functor C Cat) : Functor (Grothendieck F) (Grothendieck (F.comp 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_map_base {C : Type u} [Category.{v, u} C] (F : Functor C Cat) {X✝ Y✝ : Grothendieck F} (f : X✝ ⟶ Y✝) : ((compAsSmallFunctorEquivalenceInverse F).map f).base = f.base

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor {C : Type u} [Category.{v, u} C] (F : Functor C Cat) : Functor (Grothendieck (F.comp Cat.asSmallFunctor)) (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} [Category.{v, u} C] (F : Functor C Cat) {X✝ Y✝ : Grothendieck (F.comp Cat.asSmallFunctor)} (f : X✝ ⟶ Y✝) : ((compAsSmallFunctorEquivalenceFunctor F).map f).base = f.base

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence {C : Type u} [Category.{v, u} C] (F : Functor C Cat) : Grothendieck (F.comp Cat.asSmallFunctor) ≌ 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} [Category.{v, u} C] (F : Functor C Cat) : (compAsSmallFunctorEquivalence F).counitIso = Iso.refl ((compAsSmallFunctorEquivalenceInverse F).comp (compAsSmallFunctorEquivalenceFunctor F))

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Grothendieck.mapWhiskerRightAsSmallFunctor {C : Type u} [Category.{v, u} C] {F G : Functor C Cat} (α : F ⟶ G) : map (whiskerRight α Cat.asSmallFunctor) ≅ (compAsSmallFunctorEquivalence F).functor.comp ((map α).comp (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 : Cat} : Functor (Functor (↑E) Cat) (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} [Category.{v, u} C] (G : Functor C (Type w)) : Functor (Grothendieck (G.comp 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} [Category.{v, u} C] (G : Functor C (Type w)) (X : Grothendieck (G.comp typeToCat)) : ((grothendieckTypeToCatFunctor G).obj X).snd = X.fiber.as

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Grothendieck.grothendieckTypeToCat {C : Type u} [Category.{v, u} C] (G : Functor C (Type w)) : Grothendieck (G.comp 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_hom_app_coe {C : Type u} [Category.{v, u} C] (G : Functor C (Type w)) (X : G.Elements) : ↑((grothendieckTypeToCat G).counitIso.hom.app X) = CategoryStruct.id X.fst

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Grothendieck.pre {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) (G : Functor D C) : Functor (Grothendieck (G.comp F)) (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_obj_fiber {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) (G : Functor D C) (X : Grothendieck (G.comp F)) : ((pre F G).obj X).fiber = X.fiber

@[simp]

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

@[simp]

theorem CategoryTheory.Grothendieck.pre_obj_base {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) (G : Functor D C) (X : Grothendieck (G.comp F)) : ((pre F G).obj X).base = G.obj X.base

@[simp]

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

@[simp]

theorem CategoryTheory.Grothendieck.pre_id {C : Type u} [Category.{v, u} C] (F : Functor C Cat) : pre F (Functor.id C) = Functor.id (Grothendieck ((Functor.id C).comp F))

def CategoryTheory.Grothendieck.preNatIso {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) {G H : Functor D C} (α : G ≅ H) : pre F G ≅ (map (whiskerRight α.hom F)).comp (pre F H)

An natural isomorphism between functors G ≅ H induces a natural isomorphism between the canonical morphism pre F G and pre F H, up to composition with Grothendieck (G ⋙ F) ⥤ Grothendieck (H ⋙ F).

Equations

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

def CategoryTheory.Grothendieck.preInv {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) (G : D ≌ C) : Functor (Grothendieck F) (Grothendieck (G.functor.comp F))

Given an equivalence of categories G, preInv _ G is the (weak) inverse of the pre _ G.functor.

Equations

• CategoryTheory.Grothendieck.preInv F G = (CategoryTheory.Grothendieck.map (CategoryTheory.whiskerRight G.counitInv F)).comp (CategoryTheory.Grothendieck.pre (G.functor.comp F) G.inverse)

theorem CategoryTheory.Grothendieck.pre_comp_map {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (G : Functor D C) {H : Functor C Cat} (α : F ⟶ H) : (pre F G).comp (map α) = (map (whiskerLeft G α)).comp (pre H G)

theorem CategoryTheory.Grothendieck.pre_comp_map_assoc {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F : Functor C Cat} (G : Functor D C) {H : Functor C Cat} (α : F ⟶ H) {E : Type u_1} [Category.{u_2, u_1} E] (K : Functor (Grothendieck H) E) : (pre F G).comp ((map α).comp K) = (map (whiskerLeft G α)).comp ((pre H G).comp K)

@[simp]

theorem CategoryTheory.Grothendieck.pre_comp {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) {E : Type u_1} [Category.{u_2, u_1} E] (G : Functor D C) (H : Functor E D) : pre F (H.comp G) = (pre (G.comp F) H).comp (pre F G)

def CategoryTheory.Grothendieck.preUnitIso {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) (G : D ≌ C) : map (whiskerRight G.unitInv (G.functor.comp F)) ≅ pre (G.functor.comp F) (G.functor.comp G.inverse)

Let G be an equivalence of categories. The functor induced via pre by G.functor ⋙ G.inverse is naturally isomorphic to the functor induced via map by a whiskered version of G's inverse unit.

Equations

• CategoryTheory.Grothendieck.preUnitIso F G = (CategoryTheory.Grothendieck.preNatIso (G.functor.comp F) G.unitIso.symm).symm

def CategoryTheory.Grothendieck.preEquivalence {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C Cat) (G : D ≌ C) : Grothendieck (G.functor.comp F) ≌ Grothendieck F

Given a functor F : C ⥤ Cat and an equivalence of categories G : D ≌ C, the functor pre F G.functor is an equivalence between Grothendieck (G.functor ⋙ F) and Grothendieck F.

Equations

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

def CategoryTheory.Grothendieck.mapWhiskerLeftIsoConjPreMap {C : Type u} [Category.{v, u} C] {D : Type u₁} [Category.{v₁, u₁} D] {F F' : Functor C Cat} (G : D ≌ C) (α : F ⟶ F') : map (whiskerLeft G.functor α) ≅ (preEquivalence F G).functor.comp ((map α).comp (preEquivalence F' G).inverse)

Let F, F' : C ⥤ Cat be functor, G : D ≌ C an equivalence and α : F ⟶ F' a natural transformation.

Left-whiskering α by G and then taking the Grothendieck construction is, up to isomorphism, the same as taking the Grothendieck construction of α and using the equivalences pre F G and pre F' G to match the expected type:

Grothendieck (G.functor ⋙ F) ≌ Grothendieck F ⥤ Grothendieck F' ≌ Grothendieck (G.functor ⋙ F')

Equations

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

def CategoryTheory.Grothendieck.ι {C : Type u} [Category.{v, u} C] (F : Functor C Cat) (c : C) : Functor (↑(F.obj c)) (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.ι_map {C : Type u} [Category.{v, u} C] (F : Functor C Cat) (c : C) {X✝ Y✝ : ↑(F.obj c)} (f : X✝ ⟶ Y✝) : (ι F c).map f = { base := CategoryStruct.id ((fun (d : ↑(F.obj c)) => { base := c, fiber := d }) X✝).base, fiber := CategoryStruct.comp (eqToHom ⋯) f }

@[simp]

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

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

def CategoryTheory.Grothendieck.ιNatTrans {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {X Y : C} (f : X ⟶ Y) : ι F X ⟶ Functor.comp (F.map f) (ι 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} [Category.{v, u} C] {F : Functor C Cat} {X Y : C} (f : X ⟶ Y) (d : ↑(F.obj X)) : ((ιNatTrans f).app d).fiber = CategoryStruct.id ((F.map f).obj ((ι F X).obj d).fiber)

@[simp]

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

def CategoryTheory.Grothendieck.functorFrom {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_2, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) : Functor (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_obj {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_2, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) (X : Grothendieck F) : (functorFrom fib hom hom_id hom_comp).obj X = (fib X.base).obj X.fiber

@[simp]

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

def CategoryTheory.Grothendieck.ιCompFunctorFrom {C : Type u} [Category.{v, u} C] {F : Functor C Cat} {E : Type u_1} [Category.{u_2, u_1} E] (fib : (c : C) → Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ Functor.comp (F.map f) (fib c')) (hom_id : ∀ (c : C), hom (CategoryStruct.id c) = eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryStruct.comp f g) = CategoryStruct.comp (hom f) (CategoryStruct.comp (whiskerLeft (F.map f) (hom g)) (eqToHom ⋯))) (c : C) : (ι F c).comp (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.

def CategoryTheory.Grothendieck.ιCompMap {C : Type u} [Category.{v, u} C] {F F' : Functor C Cat} (α : F ⟶ F') (c : C) : (ι F c).comp (map α) ≅ Functor.comp (α.app c) (ι F' c)

The fiber inclusion ι F c composed with map α is isomorphic to α.app c ⋙ ι F' c.

Equations

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

@[simp]

theorem CategoryTheory.Grothendieck.ιCompMap_hom_app_base {C : Type u} [Category.{v, u} C] {F F' : Functor C Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((ιCompMap α c).hom.app X).base = CategoryStruct.id c

@[simp]

theorem CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber {C : Type u} [Category.{v, u} C] {F F' : Functor C Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((ιCompMap α c).hom.app X).fiber = eqToHom ⋯

@[simp]

theorem CategoryTheory.Grothendieck.ιCompMap_inv_app_base {C : Type u} [Category.{v, u} C] {F F' : Functor C Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((ιCompMap α c).inv.app X).base = CategoryStruct.id c

@[simp]

theorem CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber {C : Type u} [Category.{v, u} C] {F F' : Functor C Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((ιCompMap α c).inv.app X).fiber = eqToHom ⋯