English
If F is comonadic and L ⋙ F has a left adjoint, then L has a left adjoint.
Русский
Если F комонадный и L ⋙ F имеет левое сопряжение, то L имеет левое сопряжение.
LaTeX
$$$$(L \\circ F) \\text{ left adjoint } \\Rightarrow L \\text{ left adjoint}.$$$$
Lean4
/-- Suppose we have a commutative square of functors
```
Q
A → B
U ↓ ↓ V
C → D
R
```
where `U` has a right adjoint, `A` has coreflexive equalizers and `V` has a right adjoint such that
each component of the counit is a regular mono.
Then `Q` has a right adjoint if `L` has a right adjoint.
See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
-/
theorem isLeftAdjoint_square_lift (Q : A ⥤ B) (V : B ⥤ D) (U : A ⥤ C) (L : C ⥤ D) (comm : U ⋙ L ≅ Q ⋙ V)
[U.IsLeftAdjoint] [V.IsLeftAdjoint] [L.IsLeftAdjoint] [∀ X, RegularMono ((Adjunction.ofIsLeftAdjoint V).unit.app X)]
[HasCoreflexiveEqualizers A] : Q.IsLeftAdjoint :=
have := ((Adjunction.ofIsLeftAdjoint (U ⋙ L)).ofNatIsoLeft comm).isLeftAdjoint
isLeftAdjoint_triangle_lift Q (Adjunction.ofIsLeftAdjoint V)
