Adjoint functor theorem #
This file proves the (general) adjoint functor theorem, in the form:
- If
G : D ⥤ Cpreserves limits andDhas limits, and satisfies the solution set condition, then it has a left adjoint:is_right_adjoint_of_preserves_limits_of_solution_set_condition.
We show that the converse holds, i.e. that if G has a left adjoint then it satisfies the solution
set condition, see solution_set_condition_of_is_right_adjoint
(the file category_theory/adjunction/limits already shows it preserves limits).
We define the solution set condition for the functor G : D ⥤ C to mean, for every object
A : C, there is a set-indexed family ${f_i : A ⟶ G (B_i)}$ such that any morphism A ⟶ G X
factors through one of the f_i.
The functor G : D ⥤ C satisfies the solution set condition if for every A : C, there is a
family of morphisms {f_i : A ⟶ G (B_i) // i ∈ ι} such that given any morphism h : A ⟶ G X,
there is some i ∈ ι such that h factors through f_i.
The key part of this definition is that the indexing set ι lives in Type v, where v is the
universe of morphisms of the category: this is the "smallness" condition which allows the general
adjoint functor theorem to go through.
If G : D ⥤ C is a right adjoint it satisfies the solution set condition.
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.