English
For each X, the pair (U' F η_X, otherMap X) is a coreflexive pair, hence has an equalizer if C has coreflexive equalizers.
Русский
Для каждого X пара (U' F η_X, другойMap X) образует coreflexive пару, следовательно существует равнозначитель при наличии в C coreflexive равнозначителей.
LaTeX
$$$$\\text{For each } X,\; (U' F \\eta_X, \\mathrm{otherMap}(X)) \\text{ is a coreflexive pair.}$$$$
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 reflexive equalizers and `V` is comonadic.
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_comonadic (Q : A ⥤ B) (V : B ⥤ D) (U : A ⥤ C) (L : C ⥤ D) (comm : U ⋙ L ≅ Q ⋙ V)
[U.IsLeftAdjoint] [ComonadicLeftAdjoint V] [L.IsLeftAdjoint] [HasCoreflexiveEqualizers A] : Q.IsLeftAdjoint :=
have := ((Adjunction.ofIsLeftAdjoint (U ⋙ L)).ofNatIsoLeft comm).isLeftAdjoint
isLeftAdjoint_triangle_lift_comonadic V
