finite_of_toPiLocalization_surjective

English

If the map to PiLocalization is surjective, then MaximalSpectrum is finite.

Русский

Если отображение в PiLocalization сюръективно, спектр максимальных идеалов конечен.

LaTeX

$$$\text{Surjective } (\mathrm{toPiLocalization}\ R) \Rightarrow \operatorname{Finite}(\mathrm{MaximalSpectrum}(R))$$$

Lean4

theorem finite_of_toPiLocalization_surjective (surj : Function.Surjective (toPiLocalization R)) :
    Finite (MaximalSpectrum 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

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