hasColimits_of_hasLimits_of_isCoseparating

English

If C has limits, is well-powered, and possesses a small coseparating set, then C has colimits.

Русский

Если категория C имеет пределы, хорошо-управляема и обладает малым coseparating набором, то у C существуют колимиты.

LaTeX

$$[HasLimits C] ∧ [WellPowered C] ∧ [Small 𝒢] ∧ IsCoseparating 𝒢 ⇒ HasColimits C$$

Lean4

/-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and
    has a small coseparating set, then it is cocomplete. -/
theorem hasColimits_of_hasLimits_of_isCoseparating [HasLimits C] [WellPowered.{v} C] {𝒢 : Set C} [Small.{v} 𝒢]
    (h𝒢 : IsCoseparating 𝒢) : HasColimits C :=
  {
    has_colimits_of_shape := fun _ _ =>
      hasColimitsOfShape_iff_isRightAdjoint_const.2 (isRightAdjoint_of_preservesLimits_of_isCoseparating h𝒢 _) }

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