English
The localization at a module of units is isomorphic to the ring itself.
Русский
Локализация по модулю единиц изоморфна самому кольцу.
LaTeX
$$$R \\cong \\mathrm{Localization}\\bigl(M\\bigr)$ when $M$ is units-localizing$$
Lean4
/-- The localization at a module of units is isomorphic to the ring. -/
noncomputable def atUnits (H : M ≤ IsUnit.submonoid R) : R ≃ₐ[R] S :=
by
refine AlgEquiv.ofBijective (Algebra.ofId R S) ⟨?_, ?_⟩
· intro x y hxy
obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy
obtain ⟨u, hu⟩ := H c.prop
rwa [← hu, Units.mul_right_inj] at eq
· intro y
obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y
obtain ⟨u, hu⟩ := H s.prop
use x * u.inv
dsimp [Algebra.ofId, RingHom.toFun_eq_coe, AlgHom.coe_mks]
rw [RingHom.map_mul, ← eq, ← hu, mul_assoc, ← RingHom.map_mul]
simp
