English
If the Zariski topology on PrimeSpectrum(R) is discrete, then the canonical map to the Pi-localization is surjective.
Русский
Если топология Зарици на PrimeSpectrum(R) дискретна, то естественный отображение в Pi-локализацию сюръективно.
LaTeX
$$$$ \\text{DiscreteTopology}(\\operatorname{PrimeSpectrum}(R)) \\;\Longrightarrow\\; \\operatorname{Surjective}(\\operatorname{toPiLocalization}(R)). $$$$
Lean4
theorem toPiLocalization_surjective_of_discreteTopology : Function.Surjective (toPiLocalization R) := fun x ↦
by
have (p : PrimeSpectrum R) : ∃ f, (basicOpen f : Set _) = { p } :=
have ⟨_, ⟨f, rfl⟩, hpf, hfp⟩ := isTopologicalBasis_basic_opens.isOpen_iff.mp (isOpen_discrete { p }) p rfl
⟨f, hfp.antisymm <| Set.singleton_subset_iff.mpr hpf⟩
choose f hf using this
let e := Equiv.ofInjective f fun p q eq ↦ Set.singleton_injective (hf p ▸ eq ▸ hf q)
have loc a : IsLocalization.AtPrime (Localization.Away a.1) (e.symm a).1 :=
(isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton <| hf _).mp <| by
simp_rw [e, Equiv.apply_ofInjective_symm]; infer_instance
let algE a :=
IsLocalization.algEquiv (e.symm a).1.primeCompl (Localization.AtPrime (e.symm a).1) (Localization.Away a.1)
have span_eq : Ideal.span (Set.range f) = ⊤ :=
iSup_basicOpen_eq_top_iff.mp <| top_unique fun p _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨p, (hf p).ge rfl⟩
replace hf a : (basicOpen a.1 : Set _) = {e.symm a} := by simp_rw [e, ← hf, Equiv.apply_ofInjective_symm]
obtain ⟨r, eq, -⟩ :=
Localization.existsUnique_algebraMap_eq_of_span_eq_top _ span_eq (fun a ↦ algE a (x _)) fun a b ↦
by
obtain rfl | ne := eq_or_ne a b; · rfl
have nil : IsNilpotent (a * b : R) :=
(basicOpen_eq_bot_iff _).mp <|
by
simp_rw [basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf, hf]
exact bot_unique (fun _ ⟨ha, hb⟩ ↦ ne <| e.symm.injective (ha.symm.trans hb))
apply (IsLocalization.subsingleton (M := .powers (a * b : R)) nil).elim
refine ⟨r, funext fun I ↦ ?_⟩
have := eq (e I)
rwa [← AlgEquiv.symm_apply_eq, AlgEquiv.commutes, e.symm_apply_apply] at this
