hasColimits_of_hasLimits_of_hasCoseparator

English

If C has limits, cocomplete, and has a small coseparator, then C has colimits.

Русский

Если C имеет пределы и кокумплетна и обладает малым coseparator, то C имеет колимиты.

LaTeX

$$HasLimits C ∧ HasCoseparator C ∧ WellPowered C ⇒ HasColimits C$$

Lean4

/-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
    has a coseparator, then it is cocomplete. -/
theorem hasColimits_of_hasLimits_of_hasCoseparator [HasLimits C] [HasCoseparator C] [WellPowered.{v} C] :
    HasColimits C :=
  hasColimits_of_hasLimits_of_isCoseparating <| isCoseparator_coseparator C

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