English
There is an order-preserving bijection between the set of minimal prime ideals of R and the set of irreducible components of Spec(R), i.e., the two are in natural correspondence with reversed order.
Русский
Существует биекция, сохраняющая порядок, между множеством минимальных идеалов-примеров кольца R и множеством неразложимых компонент спектра Spec(R) (с противоположным порядком).
LaTeX
$$$\\mathrm{MinPrimes}(R) \\cong_{\\text{ord}} (\\mathrm{IrrComponents}(\\mathrm{Spec} R))^{\\mathrm{op}}$$$
Lean4
/-- Zero loci of minimal prime ideals of `R` are irreducible components in `Spec R` and any
irreducible component is a zero locus of some minimal prime ideal. -/
@[stacks 00ES]
protected def _root_.minimalPrimes.equivIrreducibleComponents :
minimalPrimes R ≃o (irreducibleComponents <| PrimeSpectrum R)ᵒᵈ :=
by
let e : {p : Ideal R | p.IsPrime ∧ ⊥ ≤ p} ≃o PrimeSpectrum R :=
⟨⟨fun x ↦ ⟨x.1, x.2.1⟩, fun x ↦ ⟨x.1, x.2, bot_le⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩, Iff.rfl⟩
rw [irreducibleComponents_eq_maximals_closed]
exact
OrderIso.setOfMinimalIsoSetOfMaximal
(e.trans
((PrimeSpectrum.pointsEquivIrreducibleCloseds R).trans
(TopologicalSpace.IrreducibleCloseds.orderIsoSubtype' (PrimeSpectrum R)).dual))
