English
If R ⋙ U has a left adjoint and U is monadic, then R has a left adjoint.
Русский
Если R ∘ U имеет левое сопряжение, а U монадический, то R имеет левое сопряжение.
LaTeX
$$$$(R \\circ U) \\text{ имеет левое сопряжение} \\Rightarrow R \\text{ имеет левое сопряжение},\\; \\text{при условии моноадъюнктности } U.$$$
Lean4
/-- If `R ⋙ U` has a left adjoint, the domain of `R` has reflexive coequalizers and `U` is a monadic
functor, then `R` has a left adjoint.
This is a special case of `isRightAdjoint_triangle_lift` which is often more useful in practice.
-/
theorem isRightAdjoint_triangle_lift_monadic (U : B ⥤ C) [MonadicRightAdjoint U] {R : A ⥤ B}
[HasReflexiveCoequalizers A] [(R ⋙ U).IsRightAdjoint] : R.IsRightAdjoint :=
by
let R' : A ⥤ _ := R ⋙ Monad.comparison (monadicAdjunction U)
rsuffices : R'.IsRightAdjoint
· let this : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := by infer_instance
refine
((Adjunction.ofIsRightAdjoint (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv)).ofNatIsoRight
?_).isRightAdjoint
exact Functor.isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm ≪≫ R.rightUnitor
let this : (R' ⋙ Monad.forget (monadicAdjunction U).toMonad).IsRightAdjoint :=
by
refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint
exact Functor.isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm
let this : ∀ X, RegularEpi ((Monad.adj (monadicAdjunction U).toMonad).counit.app X) :=
by
intro X
simp only [Monad.adj_counit]
exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩
exact isRightAdjoint_triangle_lift R' (Monad.adj _)
