English
For a multivariate polynomial f ∈ MvPolynomial σ R and a prime p ∈ Spec R, p lies in the comap along C of the basic open set defined by f if and only if there exists an index i such that the coefficient f.i is not contained in p.
Русский
Пусть f ∈ MvPolynomial σ R и p ∈ Spec R. Тогда p принадлежит обратному изображению по C базового открытого множества, определяемого f, тогда существует индекс i such that коэффициент f_i не принадлежит p.
LaTeX
$$$x \\in \\mathrm{comap} (C\\ (\\sigma := \\sigma)) '' \\mathrm{basicOpen}\\ f \\iff \\exists i,\\ f.coeff i \\notin x.asIdeal$$$
Lean4
theorem mem_image_comap_C_basicOpen (f : MvPolynomial σ R) (x : PrimeSpectrum R) :
x ∈ comap (C (σ := σ)) '' basicOpen f ↔ ∃ i, f.coeff i ∉ x.asIdeal := by
classical
trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
· refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)
let e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField :=
scalarRTensorAlgEquiv
rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
change (e.toAlgHom.toRingHom).comp (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0
congr!
ext
· simp [scalarRTensorAlgEquiv, e, coeff_map, Algebra.smul_def, apply_ite (f := algebraMap _ _)]
· simp [e, scalarRTensorAlgEquiv, coeff_map, coeff_X']
· simp [MvPolynomial.ext_iff, coeff_map]
