hasLimits_of_hasColimits_of_isSeparating

English

If C has colimits, is cocomplete in the dual sense, and has a small separating set, then C has limits.

Русский

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

LaTeX

$$HasColimits C ∧ WellPowered(Cᵒᵖ) ∧ Small 𝒢 ∧ IsSeparating 𝒢 ⇒ HasLimits C$$

Lean4

/-- A consequence of the special adjoint functor theorem: if `C` is cocomplete, well-copowered and
    has a small separating set, then it is complete. -/
theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ] {𝒢 : Set C} [Small.{v} 𝒢]
    (h𝒢 : IsSeparating 𝒢) : HasLimits C :=
  {
    has_limits_of_shape := fun _ _ =>
      hasLimitsOfShape_iff_isLeftAdjoint_const.2 (isLeftAdjoint_of_preservesColimits_of_isSeparating h𝒢 _) }

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