hasColimitsOfShape_of_finallySmall

English

If J is initially small, then HasColimitsOfShape J C holds for any C with colimits of appropriate size.

Русский

Если J первоначально мал, то для любого C, имеющего колимиты заданного размера, существуют колимиты формы J в C.

LaTeX

$$$[\\text{InitiallySmall } J] \\Rightarrow \\text{HasColimitsOfShape } J\\; C$$$

Lean4

theorem hasColimitsOfShape_of_finallySmall (J : Type u) [Category.{v} J] [FinallySmall.{w} J] (C : Type u₁)
    [Category.{v₁} C] [HasColimitsOfSize.{w, w} C] : HasColimitsOfShape J C :=
  Final.hasColimitsOfShape_of_final (fromFinalModel J)

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