English
Let A be a domain with fraction field K, and S a submonoid of A such that S contains no zero divisors. The carrier of the subalgebra Localization.subalgebra.ofField K S hS is precisely the set of elements x ∈ K of the form algebraMap A K a · (algebraMap A K s)^{-1} with a, s ∈ A and s ∈ S.
Русский
Пусть A — домен с полем дробей K, и S — подмонад A без нулевых делителей. Образ подалгебры Localization.subalgebra.ofField K S hS есть множество элементов x ∈ K вида x = algebraMap A K a · (algebraMap A K s)^{-1} с a, s ∈ A и s ∈ S.
LaTeX
$$$$ \operatorname{Localization.subalgebra.ofField} K S hS = \{ x \,|\, \exists a,s \in A, s \in S, x = \operatorname{algebraMap} A K a \cdot (\operatorname{algebraMap} A K s)^{-1} \} $$$$
Lean4
/-- Given a domain `A` with fraction field `K`, and a submonoid `S` of `A` which
contains no zero divisor, this is the localization of `A` at `S`, considered as
a subalgebra of `K` over `A`.
The carrier of this subalgebra is defined as the set of all `x : K` of the form
`algebraMap A K a * (algebraMap A K s)⁻¹` where `a s : A` and `s ∈ S`.
-/
noncomputable def ofField : Subalgebra A K :=
(mapToFractionRing K S (Localization S) hS).range.copy
{x | ∃ (a s : A) (_ : s ∈ S), x = algebraMap A K a * (algebraMap A K s)⁻¹} <|
by
ext
symm
apply mem_range_mapToFractionRing_iff_ofField
