hasColimit — Mathlib

English

For CostructuredArrow G X, under suitable hypotheses, a colimit exists for any diagram F: J ⥤ CostructuredArrow G X.

Русский

Для CostructuredArrow G X при заданных условиях существует колимит для любой диаграммы F: J ⥤ CostructuredArrow G X.

LaTeX

$$$\\operatorname{HasColimit}(F)$$$

Lean4

instance hasColimit [i₁ : HasColimit (F ⋙ proj G X)] [i₂ : PreservesColimit (F ⋙ proj G X) G] : HasColimit F :=
  by
  haveI : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) := i₁
  haveI : PreservesColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) _ := i₂
  apply Comma.hasColimit

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