radical_le_vanishingIdeal_zeroLocus

English

For any ideal I in the polynomial ring, its radical is contained in the vanishing ideal of the zero locus of I.

Русский

Для любого идеала I в многочленном кольце его радикал содержится в нулевом идеале множества нулей I.

LaTeX

$$I.radical \le \operatorname{vanishingIdeal}(k, \operatorname{zeroLocus}(K, I))$$

Lean4

theorem radical_le_vanishingIdeal_zeroLocus (I : Ideal (MvPolynomial σ k)) :
    I.radical ≤ vanishingIdeal k (zeroLocus K I) := by
  intro p hp x hx
  rw [← mem_vanishingIdeal_singleton_iff]
  rw [radical_eq_sInf] at hp
  refine
    (mem_sInf.mp hp)
      ⟨le_trans (le_vanishingIdeal_zeroLocus I) (vanishingIdeal_anti_mono fun y hy => hy.symm ▸ hx), inferInstance⟩

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