English
For a finite index set, every prime in the product has a component arising from an evaluation at an index i; there exists i and q such that (Pi.evalRingHom R i).specComap q = p.
Русский
Для конечного индекса существует i и q такие, что (Pi.evalRingHom R i).specComap q = p.
LaTeX
$$$\\exists i,\\exists q,\\ (\\Pi_{i}. R_i).\\text{evalRingHom } R i\\, .\\text{specComap } q = p$$$
Lean4
theorem exists_comap_evalRingHom_eq {ι : Type*} {R : ι → Type*} [∀ i, CommRing (R i)] [Finite ι]
(p : PrimeSpectrum (Π i, R i)) : ∃ (i : ι) (q : PrimeSpectrum (R i)), (Pi.evalRingHom R i).specComap q = p := by
classical
cases nonempty_fintype ι
let e (i) : Π i, R i := Function.update 1 i 0
have H : ∏ i, e i = 0 := by
ext j
rw [Finset.prod_apply, Pi.zero_apply, Finset.prod_eq_zero (Finset.mem_univ j)]
simp [e]
obtain ⟨i, hi⟩ : ∃ i, e i ∈ p.asIdeal := by simpa [← H, Ideal.IsPrime.prod_mem_iff] using p.asIdeal.zero_mem
let h₁ : Function.Surjective (Pi.evalRingHom R i) := RingHomSurjective.is_surjective
have h₂ : RingHom.ker (Pi.evalRingHom R i) ≤ p.asIdeal :=
by
intro x hx
convert p.asIdeal.mul_mem_left x hi
ext j
by_cases hj : i = j
· subst hj; simpa [e]
· simp [e, Function.update_of_ne (.symm hj)]
have : (p.asIdeal.map (Pi.evalRingHom R i)).comap (Pi.evalRingHom R i) = p.asIdeal := by
rwa [Ideal.comap_map_of_surjective _ h₁, sup_eq_left]
exact ⟨i, ⟨_, Ideal.map_isPrime_of_surjective h₁ h₂⟩, PrimeSpectrum.ext this⟩
