English
Let F: C → D be a functor that preserves colimits. If C is cocomplete, well-copowered, and has a small separating set, then F has a right adjoint.
Русский
Пусть F: C → D — функтор, сохраняющий колимиты. Если C кокумплета, хорошо-конапowered и имеет небольшой разделяющий набор, то F имеет правый сопряжённый.
LaTeX
$$$\text{HasColimits}(C) \land \text{WellPowered}(C^{\mathrm{op}}) \land \exists 𝒢 \subseteq C \\left( \text{Small}(𝒢) \land \text{IsSeparating}(𝒢) \right) \land \text{PreservesColimits}(F) \Rightarrow F \text{ IsLeftAdjoint}?\,$$$
Lean4
/-- The special adjoint functor theorem: if `F : C ⥤ D` preserves colimits and `C` is cocomplete,
well-copowered and has a small separating set, then `F` has a right adjoint.
-/
theorem isLeftAdjoint_of_preservesColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ] {𝒢 : Set C}
[Small.{v} 𝒢] (h𝒢 : IsSeparating 𝒢) (F : C ⥤ D) [PreservesColimits F] : F.IsLeftAdjoint :=
have : ∀ A, HasTerminal (CostructuredArrow F A) := fun A =>
hasTerminal_of_isSeparating (CostructuredArrow.isSeparating_proj_preimage F A h𝒢)
isLeftAdjoint_of_costructuredArrowTerminals _
