discreteTopology_iff_toPiLocalization_surjective

English

The Zariski topology on PrimeSpectrum(R) is discrete if and only if the map toPiLocalization(R) is surjective.

Русский

Топология Зарици на PrimeSpectrum(R) дискретна тогда и только тогда, когда отображение toPiLocalization(R) сюръективно.

LaTeX

$$$$ \operatorname{DiscreteTopology}(\operatorname{PrimeSpectrum}(R)) \iff \operatorname{Surjective}(\operatorname{toPiLocalization}(R)). $$$$

Lean4

theorem discreteTopology_iff_toPiLocalization_surjective {R} [CommSemiring R] :
    DiscreteTopology (PrimeSpectrum R) ↔ Function.Surjective (toPiLocalization R) :=
  ⟨fun _ ↦ toPiLocalization_surjective_of_discreteTopology _, discreteTopology_of_toLocalization_surjective⟩

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