English
Let F: C → Cat and G: Grothendieck F → H. Assume that for every morphism f: X → Y in C, the functor F.map f followed by Grothendieck.ι F Y and then G has a colimit. Then for every X in C, the functor Grothendieck.ι F X followed by G has a colimit in H.
Русский
Пусть F: C → Cat и G: конструкция Гротендика F → H. Предположим, что для каждого морфизма f: X → Y в C композиция F.map f ⋙ Grothendieck.ι F Y ⋙ G обладает колимитом. Тогда для каждого X в C существует колимит функции Grothendieck.ι F X ⋙ G.
LaTeX
$$$\left( \forall X,Y \in \mathrm{Obj}(C), \ f:X \to Y, \mathrm{HasColimit}\big(F.map f \circ \iota_F Y \circ G\big) \right) \Rightarrow \forall X, \mathrm{HasColimit}\big(\iota_F X \circ G\big).$$$
Lean4
@[local instance]
theorem hasColimit_ι_comp : ∀ X, HasColimit (Grothendieck.ι F X ⋙ G) := fun X =>
hasColimit_of_iso (F := F.map (𝟙 _) ⋙ Grothendieck.ι F X ⋙ G) <|
(leftUnitor (Grothendieck.ι F X ⋙ G)).symm ≪≫ (isoWhiskerRight (eqToIso (F.map_id X).symm) (Grothendieck.ι F X ⋙ G))
