English
There is an ess-surjectivity instance for the Monad.comparison of a reflective adjunction.
Русский
Существование эс-сюръективности для сопоставления монад отражательных сопряжений.
LaTeX
$$$$\\text{EssSurj}(\\mathrm{Monad.comparison}(\\mathrm{reflectorAdjunction } R))$$$$
Lean4
instance comparison_essSurj [Reflective R] : (Monad.comparison (reflectorAdjunction R)).EssSurj :=
by
refine ⟨fun X => ⟨(reflector R).obj X.A, ⟨?_⟩⟩⟩
symm
refine Monad.Algebra.isoMk ?_ ?_
· exact asIso ((reflectorAdjunction R).unit.app X.A)
dsimp only [Functor.comp_map, Monad.comparison_obj_a, asIso_hom, Functor.comp_obj, Monad.comparison_obj_A,
Adjunction.toMonad_coe]
rw [← cancel_epi ((reflectorAdjunction R).unit.app X.A)]
dsimp only [Functor.id_obj, Functor.comp_obj]
rw [Adjunction.unit_naturality_assoc, Adjunction.right_triangle_components, comp_id]
apply (X.unit_assoc _).symm
