vanishingIdeal_isIrreducible — Mathlib

English

The image of irreducible sets under vanishingIdeal equals the set of prime ideals.

Русский

Образ ирредуцируемых подмножеств по vanishingIdeal совпадает с множеством простых идеалов.

LaTeX

$$$\\operatorname{vanishingIdeal}\\bigl(\\operatorname{image}(\\operatorname{PrimeSpectrum}, \\{s \\mid \\mathrm{IsIrreducible}(s)\\})\\bigr) = \\{P \\mid PIsPrime\\}$$$

Lean4

theorem vanishingIdeal_isIrreducible : vanishingIdeal (R := R) '' {s | IsIrreducible s} = {P | P.IsPrime} :=
  Set.ext fun I ↦
    ⟨fun ⟨_, hs, e⟩ ↦ e ▸ isIrreducible_iff_vanishingIdeal_isPrime.mp hs, fun h ↦
      ⟨zeroLocus I, (isIrreducible_zeroLocus_iff_of_radical _ h.isRadical).mpr h,
        (vanishingIdeal_zeroLocus_eq_radical I).trans h.radical⟩⟩

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