finite_of_toPiLocalization_surjective

English

Let R be a commutative semiring. If the pi-localization map toPiLocalization R is onto, then the prime spectrum of R is finite.

Русский

Пусть R — коммутативное полукольцо. Если отображение к локализации поPi сюрьективно, то множество спектра простых идеалов кольца R конечно.

LaTeX

$$$\\\\operatorname{Surjective}(\\\\operatorname{toPiLocalization}(R)) \\\\Rightarrow \\\\operatorname{Finite}(\\\\operatorname{PrimeSpectrum}(R))$$$

Lean4

theorem finite_of_toPiLocalization_surjective (surj : Function.Surjective (toPiLocalization R)) :
    Finite (PrimeSpectrum R) :=
  by
  replace surj := (mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩).2.comp surj
  rw [← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
  exact finite_of_toPiLocalization_pi_surjective surj.of_comp

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