English
Let {R_i} be a family of local rings with Krull dimension at most 0. For each i, there is a map R_i → S_i. Then the coordinate-wise product map ∏_i R_i → ∏_i S_i, given by composing evaluation with the algebra maps, is surjective. In particular, the natural map sending (r_i)_i to (f_i(r_i))_i is surjective when each R_i is local of Krull dimension ≤ 0.
Русский
Пусть {R_i} — семейство локальных колец с размерностью Канка (Крулль) не более 0. Для каждого i имеется отображение R_i → S_i. Тогда покомпонентное отображение ∏_i R_i → ∏_i S_i, задаваемое как композиция оценки и алгебраических отображений, сюръективно. В частности, естественное отображение (r_i)_i ↦ (f_i(r_i))_i сюръективно при каждом R_i локально и KrullDim(R_i) ≤ 0.
LaTeX
$$$\\prod_{i} R_i \\xrightarrow{\\;\\prod_i (\\alpha_i\\circ \\pi_i)\\; } \\prod_i S_i \\quad \\text{is surjective}$$$
Lean4
theorem surjective_piRingHom_algebraMap_comp_piEvalRingHom [∀ i, Ring.KrullDimLE 0 (R i)] [∀ i, IsLocalRing (R i)] :
Surjective (Pi.ringHom (fun i ↦ (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i))) :=
by
apply Surjective.piMap (fun i ↦ ?_)
by_cases h₀ : (0 : R i) ∈ (M.map (Pi.evalRingHom R i))
· have := uniqueOfZeroMem h₀ (S := (S i))
exact surjective_to_subsingleton (algebraMap (R i) (S i))
· exact (IsLocalization.atUnits _ _ (by simpa)).surjective
