(Co)limits on the (strict) Grothendieck Construction

• Shows that if a functor G : Grothendieck F ⥤ H, with F : C ⥤ Cat, has a colimit, and every fiber of G has a colimit, then so does the fiberwise colimit functor C ⥤ H.
• Vice versa, if each fiber of G has a colimit and the fiberwise colimit functor has a colimit, then G has a colimit.
• Shows that colimits of functors on the Grothendieck construction are colimits of "fibered colimits", i.e. of applying the colimit to each fiber of the functor.
• Derives HasColimitsOfShape (Grothendieck F) H with F : C ⥤ Cat from the presence of colimits on each fiber shape F.obj X and on the base category C.

theorem CategoryTheory.Limits.hasColimit_ι_comp {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (X : C) : HasColimit ((Grothendieck.ι F X).comp G)

noncomputable def CategoryTheory.Limits.fiberwiseColimit {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] : Functor C H

A functor taking a colimit on each fiber of a functor G : Grothendieck F ⥤ H.

@[simp]

theorem CategoryTheory.Limits.fiberwiseColimit_map {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] {X Y : C} (f : X ⟶ Y) : (fiberwiseColimit G).map f = CategoryStruct.comp (colimMap (CategoryStruct.comp (Functor.whiskerRight (Grothendieck.ιNatTrans f) G) ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom)) (colimit.pre ((Grothendieck.ι F Y).comp G) (F.map f).toFunctor)

@[simp]

theorem CategoryTheory.Limits.fiberwiseColimit_obj {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (X : C) : (fiberwiseColimit G).obj X = colimit ((Grothendieck.ι F X).comp G)

noncomputable def CategoryTheory.Limits.fiberwiseColim {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C Cat) (H : Type u₂) [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] : Functor (Functor (Grothendieck F) H) (Functor C H)

Similar to colimit and colim, taking fiberwise colimits is a functor (Grothendieck F ⥤ H) ⥤ (C ⥤ H) between functor categories.

@[simp]

theorem CategoryTheory.Limits.fiberwiseColim_obj {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C Cat) (H : Type u₂) [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] (G : Functor (Grothendieck F) H) : (fiberwiseColim F H).obj G = fiberwiseColimit G

@[simp]

theorem CategoryTheory.Limits.fiberwiseColim_map_app {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C Cat) (H : Type u₂) [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] {X✝ Y✝ : Functor (Grothendieck F) H} (α : X✝ ⟶ Y✝) (c : C) : ((fiberwiseColim F H).map α).app c = colim.map ((Grothendieck.ι F c).whiskerLeft α)

noncomputable def CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] : G ⟶ (Grothendieck.forget F).comp (fiberwiseColimit G)

Every functor G : Grothendieck F ⥤ H induces a natural transformation from G to the composition of the forgetful functor on Grothendieck F with the fiberwise colimit on G.

@[simp]

theorem CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit_app {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (X : Grothendieck F) : (natTransIntoForgetCompFiberwiseColimit G).app X = colimit.ι ((Grothendieck.ι F X.base).comp G) X.fiber

noncomputable def CategoryTheory.Limits.coconeFiberwiseColimitOfCocone {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] {G : Functor (Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (c : Cocone G) : Cocone (fiberwiseColimit G)

A cocone on a functor G : Grothendieck F ⥤ H induces a cocone on the fiberwise colimit on G.

@[simp]

theorem CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_pt {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] {G : Functor (Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (c : Cocone G) : (coconeFiberwiseColimitOfCocone c).pt = c.pt

@[simp]

theorem CategoryTheory.Limits.coconeFiberwiseColimitOfCocone_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] {G : Functor (Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (c : Cocone G) (X : C) : (coconeFiberwiseColimitOfCocone c).ι.app X = colimit.desc ((Grothendieck.ι F X).comp G) (Cocone.whisker (Grothendieck.ι F X) c)

noncomputable def CategoryTheory.Limits.isColimitCoconeFiberwiseColimitOfCocone {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] {G : Functor (Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] {c : Cocone G} (hc : IsColimit c) : IsColimit (coconeFiberwiseColimitOfCocone c)

If c is a colimit cocone on G : Grothendieck F ⥤ H, then the induced cocone on the fiberwise colimit on G is a colimit cocone, too.

theorem CategoryTheory.Limits.hasColimit_fiberwiseColimit {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] [HasColimit G] : HasColimit (fiberwiseColimit G)

noncomputable def CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] {G : Functor (Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (c : Cocone (fiberwiseColimit G)) : Cocone G

For a functor G : Grothendieck F ⥤ H, every cocone over fiberwiseColimit G induces a cocone over G itself.

@[simp]

theorem CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_pt {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] {G : Functor (Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (c : Cocone (fiberwiseColimit G)) : (coconeOfCoconeFiberwiseColimit c).pt = c.pt

@[simp]

theorem CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] {G : Functor (Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] (c : Cocone (fiberwiseColimit G)) (X : Grothendieck F) : (coconeOfCoconeFiberwiseColimit c).ι.app X = CategoryStruct.comp (colimit.ι ((Grothendieck.ι F X.base).comp G) X.fiber) (c.ι.app X.base)

noncomputable def CategoryTheory.Limits.isColimitCoconeOfFiberwiseCocone {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] {G : Functor (Grothendieck F) H} [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] {c : Cocone (fiberwiseColimit G)} (hc : IsColimit c) : IsColimit (coconeOfCoconeFiberwiseColimit c)

If a cocone c over a functor G : Grothendieck F ⥤ H is a colimit, then the induced cocone coconeOfFiberwiseCocone G c

theorem CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] [HasColimit (fiberwiseColimit G)] : HasColimit G

We can infer that a functor G : Grothendieck F ⥤ H, with F : C ⥤ Cat, has a colimit from the fact that each of its fibers has a colimit and that these fiberwise colimits, as a functor C ⥤ H have a colimit.

noncomputable def CategoryTheory.Limits.colimitFiberwiseColimitIso {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] [HasColimit (fiberwiseColimit G)] : colimit (fiberwiseColimit G) ≅ colimit G

For every functor G on the Grothendieck construction Grothendieck F, if G has a colimit and every fiber of G has a colimit, then taking this colimit is isomorphic to first taking the fiberwise colimit and then the colimit of the resulting functor.

@[simp]

theorem CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] [HasColimit (fiberwiseColimit G)] (X : C) (d : ↑(F.obj X)) : CategoryStruct.comp (colimit.ι ((Grothendieck.ι F X).comp G) d) (CategoryStruct.comp (colimit.ι (fiberwiseColimit G) X) (colimitFiberwiseColimitIso G).hom) = colimit.ι G { base := X, fiber := d }

@[simp]

theorem CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] [HasColimit (fiberwiseColimit G)] (X : C) (d : ↑(F.obj X)) {Z : H} (h : colimit G ⟶ Z) : CategoryStruct.comp (colimit.ι ((Grothendieck.ι F X).comp G) d) (CategoryStruct.comp (colimit.ι (fiberwiseColimit G) X) (CategoryStruct.comp (colimitFiberwiseColimitIso G).hom h)) = CategoryStruct.comp (colimit.ι G { base := X, fiber := d }) h

@[simp]

theorem CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] [HasColimit (fiberwiseColimit G)] (X : Grothendieck F) : CategoryStruct.comp (colimit.ι G X) (colimitFiberwiseColimitIso G).inv = CategoryStruct.comp (colimit.ι ((Grothendieck.ι F X.base).comp G) X.fiber) (colimit.ι (fiberwiseColimit G) X.base)

@[simp]

theorem CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] (G : Functor (Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor.comp ((Grothendieck.ι F Y).comp G))] [HasColimit (fiberwiseColimit G)] (X : Grothendieck F) {Z : H} (h : colimit (fiberwiseColimit G) ⟶ Z) : CategoryStruct.comp (colimit.ι G X) (CategoryStruct.comp (colimitFiberwiseColimitIso G).inv h) = CategoryStruct.comp (colimit.ι ((Grothendieck.ι F X.base).comp G) X.fiber) (CategoryStruct.comp (colimit.ι (fiberwiseColimit G) X.base) h)

instance CategoryTheory.Limits.hasColimitsOfShape_grothendieck {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] [∀ (X : C), HasColimitsOfShape (↑(F.obj X)) H] [HasColimitsOfShape C H] : HasColimitsOfShape (Grothendieck F) H

noncomputable def CategoryTheory.Limits.fiberwiseColimCompColimIso {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] [HasColimitsOfShape C H] : (fiberwiseColim F H).comp colim ≅ colim

The isomorphism colimitFiberwiseColimitIso induces an isomorphism of functors (J ⥤ C) ⥤ C between fiberwiseColim F H ⋙ colim and colim.

@[simp]

theorem CategoryTheory.Limits.fiberwiseColimCompColimIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] [HasColimitsOfShape C H] (X : Functor (Grothendieck F) H) : fiberwiseColimCompColimIso.hom.app X = (colimitFiberwiseColimitIso X).hom

@[simp]

theorem CategoryTheory.Limits.fiberwiseColimCompColimIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] [HasColimitsOfShape C H] (X : Functor (Grothendieck F) H) : fiberwiseColimCompColimIso.inv.app X = (colimitFiberwiseColimitIso X).inv

noncomputable def CategoryTheory.Limits.fiberwiseColimCompEvaluationIso {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] (c : C) : (fiberwiseColim F H).comp ((evaluation C H).obj c) ≅ ((Functor.whiskeringLeft (↑(F.obj c)) (Grothendieck F) H).obj (Grothendieck.ι F c)).comp colim

Composing fiberwiseColim F H with the evaluation functor (evaluation C H).obj c is naturally isomorphic to precomposing the Grothendieck inclusion Grothendieck.ι to colim.

@[simp]

theorem CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] (c : C) (X : Functor (Grothendieck F) H) : (fiberwiseColimCompEvaluationIso c).inv.app X = CategoryStruct.id (colimit ((Grothendieck.ι F c).comp X))

@[simp]

theorem CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C Cat} {H : Type u₂} [Category.{v₂, u₂} H] [∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H] (c : C) (X : Functor (Grothendieck F) H) : (fiberwiseColimCompEvaluationIso c).hom.app X = CategoryStruct.id (colimit ((Grothendieck.ι F c).comp X))