English
If I is a maximal ideal in R_i, then its comap via the i-th Pi-evaluation map into the product ∏ R_i is maximal there as well.
Русский
Если I максимальный идеал в R_i, то его предобраз через i-й Pi-оценку в произведении остаётся максимальным.
LaTeX
$$$\forall i, I_i.IsMaximal \Rightarrow (I_i.comap (\Pi^{\mathrm{eval}}_{R,i})).IsMaximal$$$
Lean4
theorem comap_piEvalRingHom {ι : Type*} {R : ι → Type*} [∀ i, Semiring (R i)] {i : ι} {I : Ideal (R i)}
(h : I.IsMaximal) : (I.comap <| Pi.evalRingHom R i).IsMaximal :=
by
refine isMaximal_iff.mpr ⟨I.ne_top_iff_one.mp h.ne_top, fun J x le hxI hxJ ↦ ?_⟩
have ⟨r, y, hy, eq⟩ := h.exists_inv hxI
classical
convert J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y) (le <| by apply update_self i y 1 ▸ hy)
ext j
obtain rfl | ne := eq_or_ne j i
· simpa [eq_comm] using eq
· simp [update_of_ne ne]
