toPiLocalization_not_surjective_of_infinite

English

If the index set is infinite, toPiLocalization is not surjective.

Русский

Если множество индексов бесконечно, то toPiLocalization не сюръективно.

LaTeX

$$$\text{Infinite } \Rightarrow \neg \bigl( \mathrm{toPiLocalization} \text{ is surjective} \bigr)$$$

Lean4

theorem toPiLocalization_not_surjective_of_infinite [Infinite ι] : ¬Function.Surjective (toPiLocalization (Π i, R i)) :=
  fun surj ↦
  MaximalSpectrum.toPiLocalization_not_surjective_of_infinite R <|
    by
    rw [← piLocalizationToMaximal_comp_toPiLocalization]
    exact (piLocalizationToMaximal_surjective _).comp surj

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