English
The localization of the subalgebra Localization.subalgebra K S hS is itself localized at S.
Русский
Локализация подсоберки Localization.subalgebra K S hS локализована по S.
LaTeX
$$$IsLocalization\\ S\\ (subalgebra K S hS)$$$
Lean4
/-- Given a commutative ring `A` with fraction ring `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
`IsLocalization.mk' K a ⟨s, _⟩`, where `s ∈ S`.
-/
noncomputable def subalgebra (hS : S ≤ A⁰) : Subalgebra A K :=
(mapToFractionRing K S (Localization S) hS).range.copy
{x | ∃ (a s : A) (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, hS hs⟩} <|
by
ext
symm
apply mem_range_mapToFractionRing_iff
