Adjoint functor theorem #
This file proves the (general) adjoint functor theorem, in the form:
- If
G : D ⥤ C
preserves limits andD
has 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
.
This file also proves the special adjoint functor theorem, in the form:
- If
G : D ⥤ C
preserves limits andD
is complete, well-powered and has a small coseparating set, thenG
has a left adjoint:is_right_adjoint_of_preserves_limits_of_is_coseparating
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.
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.
Equations
- category_theory.is_right_adjoint_of_preserves_limits_of_is_coseparating h𝒢 G = have this : ∀ (A : C), category_theory.limits.has_initial (category_theory.structured_arrow A G), from _, category_theory.is_right_adjoint_of_structured_arrow_initials G _
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.
Equations
- category_theory.is_left_adjoint_of_preserves_colimits_of_is_separatig h𝒢 F = have this : ∀ (A : D), category_theory.limits.has_terminal (category_theory.costructured_arrow F A), from _, category_theory.is_left_adjoint_of_costructured_arrow_terminals F _