hasColimitsOfShape — Mathlib

English

If J is a shape with colimits in A and B, and L preserves colimits of shape J, then the comma category has colimits of shape J.

Русский

Если у A и B есть колимиты формы J и L сохраняет колимиты формы J, то у Comma L R есть колимиты формы J.

LaTeX

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

Lean4

instance hasColimitsOfShape [HasColimitsOfShape J A] [HasColimitsOfShape J B] [PreservesColimitsOfShape J L] :
    HasColimitsOfShape J (Comma L R) where

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