isIso_unit_of_iso — Mathlib

English

If R is a reflective functor, the multiplication μ of the associated monad is an isomorphism.

Русский

Если R — отражательная функция, то умножение μ соответствующей монады является изоморфизмом.

LaTeX

$$$$\\mu \\text{ is an isomorphism for }(\\mathrm{toMonad}(\\mathrm{reflectorAdjunction}(R))).$$$$

Lean4

theorem isIso_unit_of_iso (adj : L ⊣ R) (i : L ⋙ R ≅ 𝟭 C) : IsIso adj.unit :=
  (inferInstanceAs (IsIso (unitAsIsoOfIso adj i).hom))

Похожие утверждения