hasColimitsOfShape_of_closedUnderColimits

English

If J has colimits in C and P is closed under colimits, then J-shaped colimits exist in P.FullSubcategory

Русский

Если J имеет колимиты в C и P замкнуто по колимитам, то колимиты над формой J существуют в P.FullSubcategory

LaTeX

$$$\\text{HasColimitsOfShape } J\, P^{\\text{FullSubcategory}}$$$

Lean4

theorem hasColimitsOfShape_of_closedUnderColimits (h : ClosedUnderColimitsOfShape J P) [HasColimitsOfShape J C] :
    HasColimitsOfShape J P.FullSubcategory :=
  { has_colimit := fun F => hasColimit_of_closedUnderColimits h F }

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