maximalSpectrumToPiLocalization_surjective_of_discreteTopology

English

If the base prime spectrum is discrete, then the map from the base ring R to the Pi-localization of its maximal spectrum is surjective.

Русский

Если базовый спектр Прима дискретен, отображение из R в Pi-локализацию максимального спектра сюръективно.

LaTeX

$$$$ \\forall y \\in \\operatorname{MaximalSpectrum.PiLocalization}(R), \\exists r \\in R:\\; \\operatorname{toPiLocalization}_R(r) = y. $$$$

Lean4

theorem maximalSpectrumToPiLocalization_surjective_of_discreteTopology :
    Function.Surjective (MaximalSpectrum.toPiLocalization R) :=
  by
  rw [← piLocalizationToMaximal_comp_toPiLocalization]
  exact (piLocalizationToMaximal_surjective R).comp (toPiLocalization_surjective_of_discreteTopology R)

Похожие утверждения