English
The map comap along the constant-coefficient map C is an open map between prime spectra.
Русский
Карта comap по константной вложенности C является открытым отображением между спектрами прим.
LaTeX
$$$\\text{OpenMap}(\\mathrm{comap}\\ (\\mathrm{R}:=R)\\ C)$$$
Lean4
theorem mem_image_comap_C_basicOpen (f : R[X]) (x : PrimeSpectrum R) :
x ∈ comap C '' basicOpen f ↔ ∃ i, f.coeff i ∉ x.asIdeal :=
by
trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0
· refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)
let e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
(Algebra.TensorProduct.comm R _ _).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
change (e.toAlgHom.toRingHom).comp (algebraMap _ _) f = 0 ↔ Polynomial.mapRingHom _ f = 0
congr!
ext1
· ext; simp [e]
· simp [e]
· simp [Polynomial.ext_iff]
