English
Let f, g be polynomials in R[X] with g monic. The subset of the prime spectrum of R[X] obtained by pulling back the difference Z(g) \ Z(f) along the natural embedding C: R → R[X] is an open subset of Spec R. In fact, it equals the complement of the zero locus of some polynomial t ∈ R[X].
Русский
Пусть f, g ∈ R[X] и g монична. Подмножество спектра простых идеалов R[X], полученное инвертированием через каноническую карту C: R → R[X разности Z(g) \ Z(f), является открытым подмножеством Spec R. Фактически, оно равно дополнению нулевой локусы некоторого тождества t ∈ R[X].
LaTeX
$$$\\operatorname{IsOpen}\\big( \\operatorname{comap} C '' (\\operatorname{zeroLocus} \\{ g \\} \\setminus \\operatorname{zeroLocus} \\{ f \\}) \\big)$$$
Lean4
theorem isOpen_image_comap_of_monic (f g : R[X]) (hg : g.Monic) :
IsOpen (comap C '' (zeroLocus { g } \ zeroLocus { f })) :=
by
obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg
rw [ht]
exact (isClosed_zeroLocus (R := R) t).isOpen_compl
