# mathlibdocumentation

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.