English
An element of the base ring maps to a unit in S if and only if it divides some element of M and that element of M is in M.
Русский
Образ элемента из R под алгебра_map равен единице в S тогда и только тогда, когда он делится на некоторый элемент M и этот элемент принадлежит M.
LaTeX
$$$\\text{IsUnit}(\\mathrm{algebraMap}\\, R S\\, x) \\iff \\exists m\\in M, x \\mid m$$$
Lean4
theorem algebraMap_isUnit_iff {x : R} : IsUnit (algebraMap R S x) ↔ ∃ m ∈ M, x ∣ m :=
by
refine ⟨fun h ↦ ?_, fun ⟨m, hm, dvd⟩ ↦ isUnit_of_dvd_unit (map_dvd _ dvd) (map_units S ⟨m, hm⟩)⟩
have ⟨s, hxs⟩ := isUnit_iff_dvd_one.mp h
have ⟨⟨r, m⟩, hrm⟩ := surj M s
apply_fun (algebraMap R S x * ·) at hrm
rw [← mul_assoc, ← hxs, one_mul, ← map_mul] at hrm
have ⟨m', eq⟩ := exists_of_eq (M := M) hrm
exact ⟨m' * m, mul_mem m'.2 m.2, _, mul_left_comm _ x _ ▸ eq⟩
