vanishingIdeal_mem_minimalPrimes — Mathlib

English

For any s ⊆ Spec(R), vanishingIdeal(s) ∈ MinPrimes(R) iff closure(s) ∈ IrrComponents(Spec(R)).

Русский

Для любого множества s ⊆ Spec(R) верно: идеал исчезновения s принадлежит MinPrimes(R) тогда и только тогда, когда замыкание s является неразложимой компонентой Spec(R).

LaTeX

$$$\\mathrm{vanishingIdeal}(s) \\in \\mathrm{MinPrimes}(R) \\iff \\overline{s} \\in \\mathrm{IrrComponents}(\\mathrm{Spec} R)$$$

Lean4

theorem vanishingIdeal_mem_minimalPrimes {s : Set (PrimeSpectrum R)} :
    vanishingIdeal s ∈ minimalPrimes R ↔ closure s ∈ irreducibleComponents (PrimeSpectrum R) :=
  by
  constructor
  · rw [← zeroLocus_minimalPrimes, ← zeroLocus_vanishingIdeal_eq_closure]
    exact Set.mem_image_of_mem _
  · rw [← vanishingIdeal_irreducibleComponents, ← vanishingIdeal_closure]
    exact Set.mem_image_of_mem _

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