English
Characterizes membership of x in the range of mapToFractionRing by existentially expressing x as IsLocalization.mk' K a ⟨s, hs⟩.
Русский
Характеризуем принадлежность $x$ диапазону mapToFractionRing через существование $a,s$ с $s∈S$ и $x=\\mathrm{IsLocalization.mk'}K a⟨s,hs⟩$.
LaTeX
$$$x \\in \\mathrm{range}(\\mathrm{mapToFractionRing}\\, K\\, S\\, B\\, hS) \\iff \\exists a,s\\in A\\; (hs\\in S)\\; x = \\mathrm{IsLocalization.mk'} K a ⟨s, hS hs⟩$$$
Lean4
theorem mem_range_mapToFractionRing_iff (B : Type*) [CommRing B] [Algebra A B] [IsLocalization S B] (hS : S ≤ A⁰)
(x : K) :
x ∈ (mapToFractionRing K S B hS).range ↔ ∃ (a s : A) (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, hS hs⟩ :=
⟨by
rintro ⟨x, rfl⟩
obtain ⟨a, s, rfl⟩ := IsLocalization.mk'_surjective S x
use a, s, s.2
apply IsLocalization.lift_mk', by
rintro ⟨a, s, hs, rfl⟩
use IsLocalization.mk' _ a ⟨s, hs⟩
apply IsLocalization.lift_mk'⟩
