discreteTopology_iff_toPiLocalization_bijective

English

A discrete Zariski topology on PrimeSpectrum(R) is equivalent to the map toPiLocalization(R) being bijective.

Русский

Дискретная топология Зарици эквивалентна биективности отображения toPiLocalization(R).

LaTeX

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

Lean4

theorem discreteTopology_iff_toPiLocalization_bijective {R} [CommSemiring R] :
    DiscreteTopology (PrimeSpectrum R) ↔ Function.Bijective (toPiLocalization R) :=
  discreteTopology_iff_toPiLocalization_surjective.trans (and_iff_right <| toPiLocalization_injective _).symm

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