English
In a domain, the infimum of the localizations of R inside its field of fractions K, over all maximal ideals, is the bottom subalgebra.
Русский
В области инфикса инфимум локализаций R внутри поля частных дробей K по всем максимальным идеалам совпадает с нижней подалгеброй.
LaTeX
$$$\bigwedge_{v \in \mathrm{MaximalSpectrum}(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 maximal ideals
viewed as subalgebras of its field of fractions. -/
theorem iInf_localization_eq_bot :
(⨅ v : MaximalSpectrum R, Localization.subalgebra.ofField K _ v.asIdeal.primeCompl_le_nonZeroDivisors) = ⊥ :=
by
ext x
rw [Algebra.mem_bot, Algebra.mem_iInf]
constructor
· contrapose
intro hrange hlocal
let denom : Ideal R := (1 : Submodule R K).comap (LinearMap.toSpanSingleton R K x)
have hdenom : (1 : R) ∉ denom := by simpa [denom] using hrange
rcases denom.exists_le_maximal (denom.ne_top_iff_one.mpr hdenom) with ⟨max, hmax, hle⟩
rcases hlocal ⟨max, hmax⟩ with ⟨n, d, hd, rfl⟩
exact
hd
(hle
⟨n, by
simp [Algebra.smul_def, mul_left_comm,
mul_inv_cancel₀ <|
(map_ne_zero_iff _ <| IsFractionRing.injective R K).mpr fun h ↦ hd (h ▸ max.zero_mem :)]⟩)
· rintro ⟨y, rfl⟩ ⟨v, hv⟩
exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩
