English
If R is a field and M does not contain 0, localizing at M does not add new elements; the map algebraMap R → R_m is bijective.
Русский
Если R — поле и 0 не лежит в M, локализация по M не добавляет новых элементов; отображение algebraMap R → R_m биективно.
LaTeX
$$$\text{localization_map_bijective }\; R \; M$$$
Lean4
/-- If `R` is a field, then localizing at a submonoid not containing `0` adds no new elements. -/
theorem localization_map_bijective {R Rₘ : Type*} [CommRing R] [CommRing Rₘ] {M : Submonoid R} (hM : (0 : R) ∉ M)
(hR : IsField R) [Algebra R Rₘ] [IsLocalization M Rₘ] : Function.Bijective (algebraMap R Rₘ) :=
by
letI := hR.toField
replace hM := le_nonZeroDivisors_of_noZeroDivisors hM
refine ⟨IsLocalization.injective _ hM, fun x => ?_⟩
obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M x
obtain ⟨n, hn⟩ := hR.mul_inv_cancel (nonZeroDivisors.ne_zero <| hM hm)
exact ⟨r * n, by rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]⟩
