English
For S with an away localization away r, the range of comap(algebraMap R S) equals the basic open set determined by r.
Русский
Для S с локализацией Away(r) диапазон comap(алгебраическая карта R → S) равен базовому открытому набору, ассоциированному с r.
LaTeX
$$$$ \\mathrm{range}(\\mathrm{comap}(\\mathrm{algebraMap}(R,S))) = \\mathrm{basicOpen}(r). $$$$
Lean4
theorem localization_away_comap_range (S : Type v) [CommSemiring S] [Algebra R S] (r : R) [IsLocalization.Away r S] :
Set.range (comap (algebraMap R S)) = basicOpen r :=
by
rw [localization_comap_range S (Submonoid.powers r)]
ext x
simp only [mem_zeroLocus, basicOpen_eq_zeroLocus_compl, SetLike.mem_coe, Set.mem_setOf_eq, Set.singleton_subset_iff,
Set.mem_compl_iff, disjoint_iff_inf_le]
constructor
· intro h₁ h₂
exact h₁ ⟨Submonoid.mem_powers r, h₂⟩
· rintro h₁ _ ⟨⟨n, rfl⟩, h₃⟩
exact h₁ (x.2.mem_of_pow_mem _ h₃)
