hasLimit — Mathlib

English

The functor Comma.snd L R preserves colimits of shape J given the appropriate shape existence.

Русский

Функтор Comma.snd сохраняет колимиты формы J при соответствующих условиях существования форм колимитов.

LaTeX

$$$\\operatorname{PreservesColimitsOfShape}(J, \\mathrm{Comma}(L,R)\\mathrm{snd})$$$

Lean4

instance hasLimit [i₁ : HasLimit (F ⋙ proj X G)] [i₂ : PreservesLimit (F ⋙ proj X G) G] : HasLimit F :=
  by
  haveI : HasLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) := i₁
  haveI : PreservesLimit (F ⋙ Comma.snd (Functor.fromPUnit X) G) _ := i₂
  apply Comma.hasLimit

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