English
The infimum of localizations of a Dedekind domain at all height-one nonzero primes, viewed as subalgebras of its fraction field, is the bottom element.
Русский
Нижняя граница локализаций по всем ненулевым примарным топам высоты1 в поле дробей равна нулю.
LaTeX
$$$\\bigwedge_{v\\in \\HeightOneSpectrum(R)} \\mathrm{Localization.subalgebra.ofField} K\\ (v.asIdeal.primeCompl\\le\\mathrm{nonZeroDivisors}) = \\bot$$$
Lean4
/-- A Dedekind domain is equal to the intersection of its localizations at all its height one
non-zero prime ideals viewed as subalgebras of its field of fractions. -/
theorem iInf_localization_eq_bot [Algebra R K] [hK : IsFractionRing R K] :
(⨅ v : HeightOneSpectrum R, Localization.subalgebra.ofField K _ v.asIdeal.primeCompl_le_nonZeroDivisors) = ⊥ :=
by
ext x
rw [Algebra.mem_iInf]
constructor
on_goal 1 => by_cases hR : IsField R
· rcases
Function.bijective_iff_has_inverse.mp
(IsField.localization_map_bijective (Rₘ := K) (flip nonZeroDivisors.ne_zero rfl : 0 ∉ R⁰) hR) with
⟨algebra_map_inv, _, algebra_map_right_inv⟩
exact fun _ => Algebra.mem_bot.mpr ⟨algebra_map_inv x, algebra_map_right_inv x⟩
all_goals rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
· exact fun hx ⟨v, hv⟩ => hx ((equivMaximalSpectrum hR).symm ⟨v, hv⟩)
· exact fun hx ⟨v, hv, hbot⟩ => hx ⟨v, hv.isMaximal hbot⟩
