vanishingIdeal_zeroLocus_eq_radical

English

The vanishing ideal of the zero locus of I equals the radical of I.

Русский

Нулевой идеал нулевой зоны I равен радикалу I.

LaTeX

$$vanishingIdeal k (zeroLocus K I) = I.radical$$

Lean4

/-- Main statement of the Nullstellensatz -/
@[simp]
theorem vanishingIdeal_zeroLocus_eq_radical (I : Ideal (MvPolynomial σ k)) :
    vanishingIdeal k (zeroLocus K I) = I.radical :=
  by
  refine le_antisymm ?_ (radical_le_vanishingIdeal_zeroLocus _)
  rw [I.radical_eq_jacobson]
  apply le_sInf
  rintro J ⟨hJI, hJ⟩
  obtain ⟨x, hx⟩ := eq_vanishingIdeal_singleton_of_isMaximal K hJ
  refine hx.symm ▸ vanishingIdeal_anti_mono fun y hy p hp => ?_
  rw [← mem_vanishingIdeal_singleton_iff, Set.mem_singleton_iff.1 hy, ← hx]
  exact hJI hp

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