Theorems · Definition · algebraic geometry

PrimeSpectrum.zeroLocusEquivIrreducibleCloseds

{R : Type u} →
  [inst : CommSemiring R] →
    (I : Set R) → ↑(PrimeSpectrum.zeroLocus I) ≃o (TopologicalSpace.IrreducibleCloseds ↑(PrimeSpectrum.zeroLocus I))ᵒᵈ

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.

Defined in: Mathlib.RingTheory.Spectrum.Prime.Topology
Cited by: 0 results in Mathlib
Foundations: Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
CommSemiringstatement and proof · cited by 10,911
Equivproof · cited by 8,337
Set.Elemstatement and proof · cited by 7,166
Equiv.symmproof · cited by 3,681
OrderDualstatement and proof · cited by 927
OrderIsostatement · cited by 874
PrimeSpectrumstatement · cited by 625
OrderDual.toDualproof · cited by 481
Equiv.transproof · cited by 337
PrimeSpectrum.zeroLocusstatement and proof · cited by 164
RelIso.toEquivproof · cited by 113

Cited by1

Results whose statement or proof uses this declaration.

Ideal.minimalPrimes.equivIrreducibleComponentsproof · cited by 0