hasLimit_cospan_forget_of_left — Mathlib

English

The forgetful functor preserves the limit of a left cospan diagram, i.e., the limit of the diagram cospan f g after forgetting is computed by the corresponding limit in the target category.

Русский

Функтор забывания сохраняет предел левого диаграммы касательной развилки, то есть предел диаграммы cospan f g после забывания вычисляется так же, как и предел в целевой категории.

LaTeX

$$$\\operatorname{HasLimit}(\\mathrm{cospan}\\ f\\ g\\;\\;\\mathrm{forget})$$$

Lean4

instance hasLimit_cospan_forget_of_left : HasLimit (cospan f g ⋙ forget) :=
  by
  have : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr)) :=
    by
    change HasLimit (cospan ((forget).map f) ((forget).map g))
    infer_instance
  apply hasLimit_of_iso (diagramIsoCospan _).symm

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