English
If the basic open D(f) is exactly the singleton {p} in PrimeSpectrum(R), then the localization away from f is equivalent to localization at the prime p in S.
Русский
Пусть D(f) в спектре PrimeSpectrum(R) состоит только из одного идеала p. Тогда локализация в Away(f) совпадает с локализацией AtPrime в S по p.
LaTeX
$$$$ ( \mathrm{basicOpen}(f).\,1 = \{p\} ) \; \Longrightarrow \; \mathrm{IsLocalization.Away}(f,S) \;\iff\; \mathrm{IsLocalization.AtPrime}(S,p.\,1). $$$$
Lean4
theorem isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton [Algebra R S] {f : R} {p : PrimeSpectrum R}
(h : (basicOpen f).1 = { p }) : IsLocalization.Away f S ↔ IsLocalization.AtPrime S p.1 :=
have : IsLocalization.AtPrime (Localization.Away f) p.1 :=
by
refine
.of_le_of_exists_dvd (.powers f) _ (Submonoid.powers_le.mpr <| by apply h ▸ Set.mem_singleton p) fun r hr ↦ ?_
contrapose! hr
simp_rw [← Ideal.mem_span_singleton] at hr
have ⟨q, prime, le, disj⟩ :=
Ideal.exists_le_prime_disjoint (Ideal.span { r }) (.powers f) (Set.disjoint_right.mpr hr)
have : ⟨q, prime⟩ ∈ (basicOpen f).1 := Set.disjoint_right.mp disj (Submonoid.mem_powers f)
rw [h, Set.mem_singleton_iff] at this
rw [← this]
exact not_not.mpr (q.span_singleton_le_iff_mem.mp le)
IsLocalization.isLocalization_iff_of_isLocalization _ _ (Localization.Away f)
