hasColimit — Mathlib

English

For any F: J ⥤ Arrow T, if HasColimit of F ⋙ fst and F ⋙ snd along with a preservation condition, then HasColimit F.

Русский

Для любой F: J ⥤ Arrow T, если существуют колимиты F ⋙ fst и F ⋙ snd и выполняется условие сохранения, то HasColimit F.

LaTeX

$$$\\text{HasColimit}(F) \\text{ при условии } \\operatorname{HasColimit}(F\\circ \\mathrm{fst}) , \\operatorname{HasColimit}(F\\circ \\mathrm{snd}) , \\operatorname{PreservesColimit}(F\\circ \\mathrm{fst},\\mathrm{Left})$$$

Lean4

instance hasColimit (F : J ⥤ Arrow T) [i₁ : HasColimit (F ⋙ leftFunc)] [i₂ : HasColimit (F ⋙ rightFunc)] :
    HasColimit F := by
  haveI : HasColimit (F ⋙ Comma.fst _ _) := i₁
  haveI : HasColimit (F ⋙ Comma.snd _ _) := i₂
  apply Comma.hasColimit

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