vanishingIdeal_support — Mathlib

English

The vanishing ideal of the support of I equals the radical of I.

Русский

Идеал исчезновения тождества на поддержке I равен радикалу I.

LaTeX

$$\\operatorname{vanishingIdeal}(\\mathrm{Supp}(I)) = \\sqrt{I}$$

Lean4

theorem vanishingIdeal_support {I : IdealSheafData X} : vanishingIdeal I.support = I.radical :=
  by
  ext U : 2
  dsimp
  rw [← vanishingIdeal_zeroLocus_eq_radical]
  congr 1
  apply U.2.fromSpec.isOpenEmbedding.injective.image_injective
  rw [Set.image_preimage_eq_inter_range, IsAffineOpen.range_fromSpec, IsAffineOpen.fromSpec_image_zeroLocus,
    coe_support_inter]

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