English
If Q ⋙ V has a left adjoint and U is monadic, then Q has a left adjoint under square hypotheses.
Русский
Если квадратнообразная диаграмма удовлетворяет условиям, что V монадически, и Q ∘ V имеет левое сопряжение, то Q имеет левое сопряжение.
LaTeX
$$$$\\text{If } Q \\circ V \\text{ has a left adjoint and } V \\text{ is monadic, then } Q \\text{ has a left adjoint}.$$$
Lean4
/-- Suppose we have a commutative square of functors
```
Q
A → B
U ↓ ↓ V
C → D
R
```
where `U` has a left adjoint, `A` has reflexive coequalizers and `V` is monadic.
Then `Q` has a left adjoint if `R` has a left adjoint.
See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
-/
theorem isRightAdjoint_square_lift_monadic (Q : A ⥤ B) (V : B ⥤ D) (U : A ⥤ C) (R : C ⥤ D) (comm : U ⋙ R ≅ Q ⋙ V)
[U.IsRightAdjoint] [MonadicRightAdjoint V] [R.IsRightAdjoint] [HasReflexiveCoequalizers A] : Q.IsRightAdjoint :=
have := ((Adjunction.ofIsRightAdjoint (U ⋙ R)).ofNatIsoRight comm).isRightAdjoint
isRightAdjoint_triangle_lift_monadic V
