English
In a commutative square of functors with certain adjoint and regular epimorphism/Coequalizer hypotheses, if R has a left adjoint, then Q has a left adjoint.
Русский
В коммутативной квадратной диаграмме из функторов при некоторых допущениях относительно сопряжений и регулярных эпиморфизмов/ко-эквалайзеров, если R имеет левое сопряжение, то Q имеет левое сопряжение.
LaTeX
$$$$\\text{If } R \\text{ has a left adjoint, then } Q \\text{ has a left adjoint},$$ under the stated square conditions.$$
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` has a left adjoint such that
each component of the counit is a regular epi.
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 (Q : A ⥤ B) (V : B ⥤ D) (U : A ⥤ C) (R : C ⥤ D) (comm : U ⋙ R ≅ Q ⋙ V)
[U.IsRightAdjoint] [V.IsRightAdjoint] [R.IsRightAdjoint]
[∀ X, RegularEpi ((Adjunction.ofIsRightAdjoint V).counit.app X)] [HasReflexiveCoequalizers A] : Q.IsRightAdjoint :=
have := ((Adjunction.ofIsRightAdjoint (U ⋙ R)).ofNatIsoRight comm).isRightAdjoint
isRightAdjoint_triangle_lift Q (Adjunction.ofIsRightAdjoint V)
