discreteTopology_of_toLocalization_surjective

English

If the Pi-localization map is surjective, then the prime spectrum of R has the discrete topology.

Русский

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

LaTeX

$$$\\operatorname{DiscreteTopology}(\\operatorname{PrimeSpectrum}(R))$$$

Lean4

theorem discreteTopology_of_toLocalization_surjective (surj : Function.Surjective (toPiLocalization R)) :
    DiscreteTopology (PrimeSpectrum R) :=
  discreteTopology_iff_finite_and_krullDimLE_zero.mpr
    ⟨finite_of_toPiLocalization_surjective surj,
      .mk₀ fun I prime ↦ isMaximal_of_toPiLocalization_surjective surj ⟨I, prime⟩⟩

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