English
The general adjoint functor theorem: if has limits and preserves limits with the solution set condition, then the functor is right adjoint.
Русский
Общая теорема о сопряженной функции: если существуют пределы и сохраняются пределы с условием решения множества, то функтор является правой сопряженной.
LaTeX
$$isRightAdjoint theorem$$
Lean4
/-- The general adjoint functor theorem says that if `G : D ⥤ C` preserves limits and `D` has them,
if `G` satisfies the solution set condition then `G` is a right adjoint.
-/
theorem isRightAdjoint_of_preservesLimits_of_solutionSetCondition [HasLimits D] [PreservesLimits G]
(hG : SolutionSetCondition G) : G.IsRightAdjoint :=
by
refine @isRightAdjointOfStructuredArrowInitials _ _ _ _ G ?_
intro A
specialize hG A
choose ι B f g using hG
let B' : ι → StructuredArrow A G := fun i => StructuredArrow.mk (f i)
have hB' : ∀ A' : StructuredArrow A G, ∃ i, Nonempty (B' i ⟶ A') :=
by
intro A'
obtain ⟨i, _, t⟩ := g _ A'.hom
exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩
obtain ⟨T, hT⟩ := has_weakly_initial_of_weakly_initial_set_and_hasProducts hB'
apply hasInitial_of_weakly_initial_and_hasWideEqualizers hT
