(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 a 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₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (F.map f) ((CategoryTheory.Grothendieck.ι F Y).comp G))] (X : C) : CategoryTheory.Limits.HasColimit ((CategoryTheory.Grothendieck.ι F X).comp G)

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

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

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (F.map f) ((CategoryTheory.Grothendieck.ι F Y).comp G))] : G ⟶ (CategoryTheory.Grothendieck.forget F).comp (CategoryTheory.Limits.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.

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

def CategoryTheory.Limits.colimitFiberwiseColimitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {H : Type u₂} [CategoryTheory.Category.{v₂, u₂} H] (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp (F.map f) ((CategoryTheory.Grothendieck.ι F Y).comp G))] [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] : CategoryTheory.Limits.colimit (CategoryTheory.Limits.fiberwiseColimit G) ≅ CategoryTheory.Limits.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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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