English
For an infinite index set ι and nontrivial components R_i, there exists a maximal ideal I of Π_i R_i that does not lie in the range of sigmaToPi.
Русский
Для бесконечного множества индексов ι и ненулевых составляющих R_i существует максимальная идеал I в Π_i R_i, которая не принадлежит диапазону sigmaToPi.
LaTeX
$$$\\exists I \\; (I \\text{ maximal}) \\; (I) \\notin \\operatorname{range}(\\operatorname{sigmaToPi} R)$$$
Lean4
/-- An infinite product of nontrivial commutative semirings has a maximal ideal outside of the
range of `sigmaToPi`, i.e. is not of the form `πᵢ⁻¹(𝔭)` for some prime `𝔭 ⊂ R i`, where
`πᵢ : (Π i, R i) →+* R i` is the projection. For a complete description of all prime ideals,
see https://math.stackexchange.com/a/1563190. -/
theorem exists_maximal_notMem_range_sigmaToPi_of_infinite :
∃ (I : Ideal (Π i, R i)) (_ : I.IsMaximal), ⟨I, inferInstance⟩ ∉ Set.range (sigmaToPi R) := by
classical
let J : Ideal (Π i, R i) := -- `J := Π₀ i, R i` is an ideal in `Π i, R i`
{ __ := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom
smul_mem' := by
rintro r _ ⟨x, rfl⟩
refine ⟨.mk x.support fun i ↦ r i * x i, funext fun i ↦ show dite _ _ _ = _ from ?_⟩
simp_rw [DFinsupp.coeFnAddMonoidHom]
refine dite_eq_left_iff.mpr fun h ↦ ?_
rw [DFinsupp.notMem_support_iff.mp h, mul_zero] }
have ⟨I, max, le⟩ :=
J.exists_le_maximal <|
(Ideal.ne_top_iff_one _).mpr <| by
-- take a maximal ideal I containing J
rintro ⟨x, hx⟩
have ⟨i, hi⟩ := x.support.exists_notMem
simpa [DFinsupp.coeFnAddMonoidHom, DFinsupp.notMem_support_iff.mp hi] using congr_fun hx i
refine
⟨I, max, fun ⟨⟨i, p⟩, eq⟩ ↦ ?_⟩
-- then I is not in the range of `sigmaToPi`
have : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal := by simpa using p.1.ne_top_iff_one.mp p.2.ne_top
rw [eq] at this
exact this (le ⟨.single i 1, rfl⟩)
