equivInvSubmonoid — Mathlib

English

There is a monoid isomorphism between the image of M in S and the inverted submonoid invSubmonoid(M,S).

Русский

Существует изоморфизм Моноида между образованием M в S и инвертированным подмоноидом invSubmonoid(M,S).

LaTeX

$$$(M.map(\mathrm{algebraMap}\,R\,S)) \cong_* \operatorname{invSubmonoid}(M,S)$$$

Lean4

/-- There is an equivalence of monoids between the image of `M` and `invSubmonoid`. -/
noncomputable abbrev equivInvSubmonoid : M.map (algebraMap R S) ≃* invSubmonoid M S :=
  ((M.map (algebraMap R S)).leftInvEquiv (submonoid_map_le_is_unit M S)).symm

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