English
Let M be a submonoid of a finite product of commutative rings {R_i} with IsLocalization data, and S' a commutative semiring. If each R_i has Krull dimension at most 0 and is local, then the canonical algebra map from the product ∏_i R_i to S' is surjective; i.e., the global map onto the localization is onto.
Русский
Пусть M — подмоном в конечном произведении коммутативных колец {R_i} с данными локализации, и S' — коммутативная полугруппа. При условии, что каждая R_i имеет размерность Крылла ≤ 0 и локальна, каноническое алгебраическое отображение from∏_i R_i в S' сюръективно.
LaTeX
$$$\\text{algebraMap}\\left(\\prod_{i=1}^n R_i\\right) \\to S'\\quad \\text{is surjective}$$$
Lean4
/-- Let `M` be a submonoid of a direct product of commutative rings `R i`.
If each `R i` has maximal nilradical then the direct product `∏ R i` surjects onto the
localization of `∏ R i` at `M`. -/
theorem algebraMap_pi_surjective_of_isLocalization [∀ i, Ring.KrullDimLE 0 (R i)] [∀ i, IsLocalRing (R i)]
[IsLocalization M S'] [Finite ι] : Surjective (algebraMap (Π i, R i) S') :=
by
intro s
set S := fun (i : ι) => Localization (M.map (Pi.evalRingHom R i))
obtain ⟨r, hr⟩ :=
surjective_piRingHom_algebraMap_comp_piEvalRingHom S M
((lift (isUnit_piRingHom_algebraMap_comp_piEvalRingHom R S M)) s)
refine ⟨r, (bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom R S _ M).injective ?_⟩
rwa [lift_eq (isUnit_piRingHom_algebraMap_comp_piEvalRingHom R S M) r]
