English
The analogous infimum statement holds for prime spectrum: the infimum of localizations at all prime ideals equals the bottom subalgebra.
Русский
Аналогично для спектра простых: инфимум локализаций по всем простым идеалам равен нижнему подалгебре.
LaTeX
$$$\bigwedge_{v \in \mathrm{PrimeSpectrum}(R)} \mathrm{Localization.subalgebra.ofField}(K, v.asIdeal.primeCompl\le\text{nonZeroDivisors}) = \bot$$$
Lean4
/-- An integral domain is equal to the intersection of its localizations at all its prime ideals
viewed as subalgebras of its field of fractions. -/
theorem iInf_localization_eq_bot :
⨅ v : PrimeSpectrum R, Localization.subalgebra.ofField K _ (v.asIdeal.primeCompl_le_nonZeroDivisors) = ⊥ :=
by
refine bot_unique (.trans (fun _ ↦ ?_) (MaximalSpectrum.iInf_localization_eq_bot R K).le)
simpa only [Algebra.mem_iInf] using fun hx ⟨v, hv⟩ ↦ hx ⟨v, hv.isPrime⟩
