Adjoint lifting #

This file gives two constructions for building left adjoints: the adjoint triangle theorem and the adjoint lifting theorem. The adjoint triangle theorem says that given a functor U : B ⥤ C with a left adjoint F such that ε_X : FUX ⟶ X is a regular epi. Then for any category A with coequalizers of reflexive pairs, a functor R : A ⥤ B has a left adjoint if (and only if) the composite R ⋙ U does. Note that the condition on U regarding ε_X is automatically satisfied in the case when U is a monadic functor, giving the corollary: monadic_adjoint_triangle_lift, i.e. if U is monadic, A has reflexive coequalizers then R : A ⥤ B has a left adjoint provided R ⋙ U does.

The adjoint lifting theorem says that given a commutative square of functors (up to isomorphism):

  Q
A → B

U ↓ ↓ V C → D R

where U and V are monadic and A has reflexive coequalizers, then if R has a left adjoint then Q has a left adjoint.

Implementation #

It is more convenient to prove this theorem by assuming we are given the explicit adjunction rather than just a functor known to be a right adjoint. In docstrings, we write (η, ε) for the unit and counit of the adjunction adj₁ : F ⊣ U and (ι, δ) for the unit and counit of the adjunction adj₂ : F' ⊣ R ⋙ U.

TODO #

Dualise to lift right adjoints through comonads (by reversing 1-cells) and dualise to lift right adjoints through monads (by reversing 2-cells), and the combination.

References #

• https://ncatlab.org/nlab/show/adjoint+triangle+theorem
• https://ncatlab.org/nlab/show/adjoint+lifting+theorem
• Adjoint Lifting Theorems for Categories of Algebras (PT Johnstone, 1975)
• A unified approach to the lifting of adjoints (AJ Power, 1988)