comap_C_mem_imageOfDf — Mathlib

English

If a prime in Spec R[x] lies outside the zero locus of f, its image under comap C lies in imageOfDf(f).

Русский

Если точка спектра полиномов лежит вне нулевого множества f, то её образ под отображением comap C принадлежит imageOfDf(f).

LaTeX

$$$I \\in (0) \\text{-locus}(f)^{c} \\Rightarrow \\text{comap C}(I) \\in \\text{imageOfDf}(f)$$$

Lean4

/-- If a point of `Spec R[x]` is not contained in the vanishing set of `f`, then its image in
`Spec R` is contained in the open set where at least one of the coefficients of `f` is non-zero.
This lemma is a reformulation of `exists_C_coeff_notMem`. -/
theorem comap_C_mem_imageOfDf {I : PrimeSpectrum R[X]} (H : I ∈ (zeroLocus { f } : Set (PrimeSpectrum R[X]))ᶜ) :
    PrimeSpectrum.comap (Polynomial.C : R →+* R[X]) I ∈ imageOfDf f :=
  exists_C_coeff_notMem (mem_compl_zeroLocus_iff_notMem.mp H)

Похожие утверждения