 Adjoint lifting theorem for monad algebra functors

For a functor between Eilenberg-Moore categories lying over a right adjoint on the base categories and compatible with the monad structures, an adjoint lifting theorem constructs a left adjoint when the required reflexive coequalizers of algebra presentations exist. Applied through power-object monadicity, this converts a left adjoint of a logical functor into a right adjoint of that logical functor. The coequalizer hypotheses are part of the theorem; commutation with the forgetful functors alone is insufficient.