English
Let A be a commutative ring, S a submonoid of A with no zero divisors, and K the fraction field of A with an A-algebra structure, together with a localization B of A at S. Then for any x in K, x lies in the range of the localization map mapToFractionRing(K,S,B,hS) if and only if there exist a ∈ A and s ∈ S with s ∈ S such that x = algebraMap A K a · (algebraMap A K s)^{-1}. Equivalently, x can be written as a/s with a ∈ A and s ∈ S.
Русский
Пусть A — коммутативное кольцо, S — подмоноид A без делителей нуля, K — поле дробей A с алгебраическим отображением A в K, и B — локализация A по S. Тогда для любого x ∈ K выполняется: x принадлежит образу локализации mapToFractionRing(K,S,B,hS) тогда и только тогда, когда существуют a ∈ A и s ∈ S с s ∈ S и x = algebraMap A K a · (algebraMap A K s)^{-1}. Иными словами, x можно записать как a/s с a ∈ A, s ∈ S.
LaTeX
$$$$ x \in \mathrm{range}(\mathrm{mapToFractionRing}\,K\,S\,B\,hS) \;\Longleftrightarrow\; \exists a \in A, \exists s \in S:\ x = (\operatorname{algebraMap} A K a) \cdot (\operatorname{algebraMap} A K s)^{-1} $$$$
Lean4
theorem mem_range_mapToFractionRing_iff_ofField (B : Type*) [CommRing B] [Algebra A B] [IsLocalization S B] (x : K) :
x ∈ (mapToFractionRing K S B hS).range ↔ ∃ (a s : A) (_ : s ∈ S), x = algebraMap A K a * (algebraMap A K s)⁻¹ :=
by
rw [mem_range_mapToFractionRing_iff]
convert Iff.rfl
congr
rw [Units.val_inv_eq_inv_val]
rfl
