nLab Freyd's adjoint functor theorem

Freyd’s adjoint functor theorem (FAFT) is a fine thing when working classically but at the same time a source of inconstructivity. It ensures that under certain assumptions on a functor F : AA->BB all presheaves of the form BB(F(-),B) or all covariant presheaves of the form BB(B,F(-)) are representable. But for getting a right or left adjoint to F one has to CHOOSE for every B a representing object R(B) or L(B), respectively, i.e. BB(F(-),B) \cong BB(-,R(B)) or BB(B,F(-)) \cong BB(L(B),_), resp. Since BB typically will be large this requires GLOBAL CHOICE, i.e. choice for classes. This principle is independent even from ZFC.

For example using FAFT G.Plotkin has shown that there exist free commutative idempotent monoids in Domains, the so called Plotkin powerdomains. But to explicitate representatives even for a restricted class of domains (SFP objects) has required quite some additional effort and ingenuity.

In geometric topos theory it goes withut saying that a (finite limit preserving) colimit preserving functor between Grothendieck toposes has always a right adjoint. The point is that the solution set condition follows from the assumption that the involved toposes are Grothendieck and thus have small generating families. But for getting the right adjoints one has to use global choice.

When working relative to a base topos SS one has to employ a fibred version of FAFT for fibrations over SS. The fibred right adjoints will not be split even if the original functors was split. That is one of the reasons why one works with fibrations and cartesian functors instead of split fibrations and split cartesian functors. For proving fibred FAFT one hast to employ strong choice principles on the meta-level, of course.

It might be interesting to investigate how choice can be avoided in these cases using the work of Ahrens, Kapulkin and Shulman on “Univalent Categories and Rezk completion”.

Thomas Streicher