instHasColimitGrothendieckFunctorCompGrothendieckProj

English

Another variant of the Grothendieck colimit injections compatibility under the functor G and L.

Русский

Еще одна версия совместимости инъекций колимита Гротендика через G и L.

LaTeX

$$$\iota_{G} X ≫ (colimitIsoColimitGrothendieck L G).inv = \iota_{(CostructuredArrow.grothendieckProj L).comp G} (\langle L.obj X, { mk (id) }\rangle)$$$

Lean4

instance : HasColimit (CostructuredArrow.grothendieckProj L ⋙ G) :=
  hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit _

Похожие утверждения