hasColimits_of_hasColimits_createsColimits

English

If F creates colimits and D has all colimits, then C has all colimits.

Русский

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

LaTeX

$$$\forall F : C \to D\, [\text{CreatesColimitsOfSize } F] \wedge [\text{HasColimitsOfSize } D] \Rightarrow [\text{HasColimitsOfSize } C]$$$

Lean4

/-- If `F` creates colimits, and `D` has all colimits, then `C` has all colimits. -/
theorem hasColimits_of_hasColimits_createsColimits (F : C ⥤ D) [HasColimitsOfSize.{w, w'} D]
    [CreatesColimitsOfSize.{w, w'} F] : HasColimitsOfSize.{w, w'} C :=
  ⟨fun _ _ => hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape F⟩

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