# Adjoint functor theorem #

This file proves the (general) adjoint functor theorem, in the form:

- If
`G : D ⥤ C`

preserves limits and`D`

has limits, and satisfies the solution set condition, then it has a left adjoint:`isRightAdjointOfPreservesLimitsOfIsCoseparating`

.

We show that the converse holds, i.e. that if `G`

has a left adjoint then it satisfies the solution
set condition, see `solutionSetCondition_of_isRightAdjoint`

(the file `CategoryTheory/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 and`D`

is complete, well-powered and has a small coseparating set, then`G`

has a left adjoint:`isRightAdjointOfPreservesLimitsOfIsCoseparating`

Finally, we prove the following corollary of the special adjoint functor theorem:

- If
`C`

is complete, well-powered and has a small coseparating set, then it is cocomplete:`hasColimits_of_hasLimits_of_isCoseparating`

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.

## Instances For

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.

## Instances For

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.

## Instances For

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.

## Instances For

A consequence of the special adjoint functor theorem: if `C`

is complete, well-powered and
has a small coseparating set, then it is cocomplete.

A consequence of the special adjoint functor theorem: if `C`

is cocomplete, well-copowered and
has a small separating set, then it is complete.