vanishingIdeal_irreducibleComponents

English

The vanishing ideal of the set of irreducible components of Spec(R) is exactly the set of minimal primes of R.

Русский

Идеал исчезновения множества неразложимых компонент спектра Spec(R) совпадает с множеством минимальныхPrime‑идеалов кольца R.

LaTeX

$$$\\mathrm{vanishingIdeal}(\\mathrm{IrrComponents}(\\mathrm{Spec} R)) = \\mathrm{MinPrimes}(R)$$$

Lean4

theorem vanishingIdeal_irreducibleComponents :
    vanishingIdeal '' (irreducibleComponents <| PrimeSpectrum R) = minimalPrimes R :=
  by
  rw [irreducibleComponents_eq_maximals_closed, minimalPrimes_eq_minimals,
    image_antitone_setOf_maximal (fun s t hs _ ↦ (vanishingIdeal_anti_mono_iff hs.1).symm), ←
    funext (@Set.mem_setOf_eq _ · Ideal.IsPrime), ← vanishingIdeal_isClosed_isIrreducible]
  rfl

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