hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape

English

If F creates colimits of shape J and D has colimits of shape J, then C has colimits of shape J.

Русский

Если F создаёт колимиты формы J, а D имеет колимиты формы J, то C имеет колимиты формы J.

LaTeX

$$$\forall F : C \to D\, [\text{HasColimitsOfShape } J D] \Rightarrow [\text{CreatesColimitsOfShape } J F] \Rightarrow \text{HasColimitsOfShape } J C$$$

Lean4

/-- If `F` creates colimits of shape `J`, and `D` has colimits of shape `J`, then
`C` has colimits of shape `J`.
-/
theorem hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (F : C ⥤ D) [HasColimitsOfShape J D]
    [CreatesColimitsOfShape J F] : HasColimitsOfShape J C :=
  ⟨fun G => hasColimit_of_created G F⟩

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