English
If U has a left adjoint F and certain regularity conditions hold, then L has a left adjoint whenever (L ⋙ F) does.
Русский
Если U имеет левое сопряжение F и выполняются условия регулярности, то L имеет левое сопряжение тогда и только тогда, когда (L ⋙ F) имеет левое сопряжение.
LaTeX
$$$$\\text{If } (L \\circ F) \\text{ is left adjoint and } \\eta \\text{ are regular monomorphisms, then } L \\text{ is left adjoint}. $$$$
Lean4
/-- The adjoint triangle theorem: Suppose `U : A ⥤ B` has a left adjoint `F` such that each unit
`η_X : X ⟶ UFX` is a regular monomorphism. Then if a category `C` has equalizers of coreflexive
pairs, then a functor `L : C ⥤ B` has a right adjoint if the composite `L ⋙ F` does.
Note the converse is true (with weaker assumptions), by `Adjunction.comp`.
See https://ncatlab.org/nlab/show/adjoint+triangle+theorem
-/
theorem isLeftAdjoint_triangle_lift {U : A ⥤ B} {F : B ⥤ A} (L : C ⥤ B) (adj₁ : F ⊣ U)
[∀ X, RegularMono (adj₁.unit.app X)] [HasCoreflexiveEqualizers C] [(L ⋙ F).IsLeftAdjoint] : L.IsLeftAdjoint where
exists_rightAdjoint :=
⟨LiftRightAdjoint.constructRightAdjoint L _ adj₁ (Adjunction.ofIsLeftAdjoint _),
⟨Adjunction.adjunctionOfEquivRight _ _⟩⟩
