hasColimitsOfSize — Mathlib

English

If A and B have colimits of all sizes of shape J and L preserves colimits of size J, then the comma category has colimits of size J.

Русский

Если A и B имеют колимиты всех размеров формы J, и L сохраняет колимиты размера J, то запятая-категория имеет колимиты размера J.

LaTeX

$$$\\operatorname{HasColimitsOfSize}(J,A) \\land \\operatorname{HasColimitsOfSize}(J,B) \\land \\operatorname{PreservesColimitsOfSize}(J,L) \\Rightarrow \\operatorname{HasColimitsOfSize}(J, \\mathrm{Comma}(L,R))$$$

Lean4

instance hasColimitsOfSize [HasColimitsOfSize.{w, w'} A] [HasColimitsOfSize.{w, w'} B]
    [PreservesColimitsOfSize.{w, w'} L] : HasColimitsOfSize.{w, w'} (Comma L R) :=
  ⟨fun _ _ => inferInstance⟩

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