English
The irreducible components of Spec(R) are exactly the zero loci of the minimal prime ideals; each minimal prime p defines V(p) which is an irreducible component, and every irreducible component arises this way.
Русский
Неразложимые компоненты Specr(R) равны нулевым множествам минимальных примитивов; каждое минимальное prime‑идеал p задаёт V(p), и каждую компоненту можно получить так.
LaTeX
$$$\\{\\mathrm{V}(\\mathfrak p) : \\mathfrak p \\in \\mathrm{MinPrimes}(R)\\} = \\mathrm{IrrComponents}(\\mathrm{Spec} R)$$$
Lean4
theorem zeroLocus_minimalPrimes : zeroLocus ∘ (↑) '' minimalPrimes R = irreducibleComponents (PrimeSpectrum R) :=
by
rw [← vanishingIdeal_irreducibleComponents, ← Set.image_comp, Set.EqOn.image_eq_self]
intro s hs
simpa [zeroLocus_vanishingIdeal_eq_closure, closure_eq_iff_isClosed] using isClosed_of_mem_irreducibleComponents s hs
