μ_iso_of_reflective — Mathlib

English

For any X in the Monad Algebra of the reflector, the unit component at X.A is an isomorphism.

Русский

Для любого X в алгебре монадного рефлектора, компонент единицы в X.A является изоморфизмом.

LaTeX

$$$$\\bigl(((\\mathrm{reflectorAdjunction } R).\\mathrm{unit}.app X.A)\\bigr) \\text{ isIso}$$$$

Lean4

instance μ_iso_of_reflective [Reflective R] : IsIso (reflectorAdjunction R).toMonad.μ :=
  by
  dsimp
  infer_instance

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