mapPiLocalization — Mathlib

English

If the toPiLocalization map is surjective, then the index set is finite (for primes).

Русский

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

LaTeX

$$$\text{Surjective } (\mathrm{toPiLocalization}((R_i)_{i\in I})) \Rightarrow \text{Finite}(I)$$$

Lean4

/-- A ring homomorphism induces a homomorphism between the products of localizations at primes. -/
noncomputable def mapPiLocalization : PiLocalization R →+* PiLocalization S :=
  Pi.ringHom fun I ↦ (Localization.localRingHom _ I.1 f rfl).comp (Pi.evalRingHom _ (f.specComap I))

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