English
Let G: D → C be a functor that preserves limits. If D has all limits, is well-powered, and has a small coseparating set, then G has a left adjoint.
Русский
Пусть G: D → C — функтор, сохраняющий пределы. Если D имеет все пределы, является хорошо-упорядоченной (well-powered) и имеет малого размера coseparating набор 𝒢, то у G существует левый сопряжённый функтор.
LaTeX
$$$\text{HasLimits}(D) \land \text{WellPowered}(D) \land \exists 𝒢 \subseteq D \left( \text{Small}(𝒢) \land \text{IsCoseparating}(𝒢) \right) \land \text{PreservesLimits}(G) \Rightarrow \exists F : C \to D,\ F \dashv G.$$$
Lean4
/-- The special adjoint functor theorem: if `G : D ⥤ C` preserves limits and `D` is complete,
well-powered and has a small coseparating set, then `G` has a left adjoint.
-/
theorem isRightAdjoint_of_preservesLimits_of_isCoseparating [HasLimits D] [WellPowered.{v} D] {𝒢 : Set D} [Small.{v} 𝒢]
(h𝒢 : IsCoseparating 𝒢) (G : D ⥤ C) [PreservesLimits G] : G.IsRightAdjoint :=
have : ∀ A, HasInitial (StructuredArrow A G) := fun A =>
hasInitial_of_isCoseparating (StructuredArrow.isCoseparating_proj_preimage A G h𝒢)
isRightAdjointOfStructuredArrowInitials _
