English
There is a natural order-preserving correspondence between the prime spectrum of a ring and the dual of the lattice of irreducible closed subsets of that spectrum, given by sending a prime p to its zero locus V(p). In particular, zero loci of prime ideals are closed irreducible sets, and conversely every closed irreducible set is the zero locus of some prime ideal.
Русский
Существует естественная порядок-однозначная корреспонденция между спектром простых идеалов кольца и дуалом помноженной решетки неразделимых замкнутых подмножеств этого спектра, заданная отображением p ↦ V(p). В частности, нуль-множества идеалов являются замкнутыми неразделимыми множествами, и наоборот каждое неразделимое замкнутое множество является нуль-множеством некоторого идеала.
LaTeX
$$$$ \operatorname{PrimeSpectrum}(R) \cong_{o} \big( \operatorname{IrreducibleCloseds}(\operatorname{PrimeSpectrum}(R)) \big)^{\mathrm{op}}. $$$$
Lean4
/-- Zero loci of prime ideals are closed irreducible sets in the Zariski topology and any closed
irreducible set is a zero locus of some prime ideal.
-/
protected def pointsEquivIrreducibleCloseds :
PrimeSpectrum R ≃o (TopologicalSpace.IrreducibleCloseds (PrimeSpectrum R))ᵒᵈ
where
__ := irreducibleSetEquivPoints.toEquiv.symm.trans OrderDual.toDual
map_rel_iff' {p q} := (RelIso.symm irreducibleSetEquivPoints).map_rel_iff.trans (le_iff_specializes p q).symm
