hasColimitCompEvaluation — Mathlib

English

If for each k the colimit of F.flip.obj k exists, then a colimit of F composed with evaluation at k exists.

Русский

Если существует колимит для каждого k у F.flip.obj k, то существует колимит для F, композиции с ev_k.

LaTeX

$$$\forall k,\ HasColimit(F.flip.obj k) \Rightarrow HasColimit\big(F \circ (\mathrm{ev}_k)\big)$$$

Lean4

instance hasColimitCompEvaluation (F : J ⥤ K ⥤ C) (k : K) [HasColimit (F.flip.obj k)] :
    HasColimit (F ⋙ (evaluation _ _).obj k) :=
  hasColimit_of_iso (F := F.flip.obj k) (Iso.refl _)

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