English
If the pi-localization map is surjective, then any prime ideal is maximal.
Русский
Если отображение локализации по квадратной группе сюръективно, то любойPrime идеал максимален.
LaTeX
$$$\forall I\in \mathrm{PrimeSpectrum}(R), I$ is maximal given surjectivity of toPiLocalization$$
Lean4
theorem isMaximal_of_toPiLocalization_surjective (surj : Function.Surjective (toPiLocalization R))
(I : PrimeSpectrum R) : I.1.IsMaximal := by
classical
have ⟨J, max, le⟩ := I.1.exists_le_maximal I.2.ne_top
obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max.isPrime⟩ 1)
by_contra h
have hJ : algebraMap _ _ r = _ := (congr_fun hr _).trans (Function.update_self ..)
have hI : algebraMap _ _ r = _ := congr_fun hr I
rw [← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl), hJ, map_one,
Function.update_of_ne] at hI
· exact one_ne_zero hI
· intro eq; have : I.1 = J := congr_arg (·.1) eq; exact h (this ▸ max)
· exact fun ⟨s, hs⟩ ↦ IsLocalization.map_units (M := I.1.primeCompl) _ ⟨s, fun h ↦ hs (le h)⟩
