Documentation

Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic

The Zariski topology on the prime spectrum of a commutative (semi)ring #

Conventions #

We denote subsets of (semi)rings with s, s', etc... whereas we denote subsets of prime spectra with t, t', etc...

Inspiration/contributors #

The contents of this file draw inspiration from https://github.com/ramonfmir/lean-scheme which has contributions from Ramon Fernandez Mir, Kevin Buzzard, Kenny Lau, and Chris Hughes (on an earlier repository).

The Zariski topology on the prime spectrum of a commutative (semi)ring is defined via the closed sets of the topology: they are exactly those sets that are the zero locus of a subset of the ring.

Equations

The antitone order embedding of closed subsets of Spec R into ideals of R.

Equations
Instances For
    theorem PrimeSpectrum.vanishingIdeal_isIrreducible {R : Type u} [CommSemiring R] :
    PrimeSpectrum.vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s} = {P : Ideal R | P.IsPrime}
    theorem PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible {R : Type u} [CommSemiring R] :
    PrimeSpectrum.vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s IsIrreducible s} = {P : Ideal R | P.IsPrime}
    Equations
    • =

    The prime spectrum of a commutative (semi)ring is a compact topological space.

    Equations
    • =
    theorem PrimeSpectrum.preimage_comap_zeroLocus_aux {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Set R) :
    (fun (y : PrimeSpectrum S) => { asIdeal := Ideal.comap f y.asIdeal, isPrime := }) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (f '' s)

    The function between prime spectra of commutative (semi)rings induced by a ring homomorphism. This function is continuous.

    Equations
    Instances For
      @[simp]
      theorem PrimeSpectrum.comap_asIdeal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (y : PrimeSpectrum S) :
      ((PrimeSpectrum.comap f) y).asIdeal = Ideal.comap f y.asIdeal
      @[simp]
      theorem PrimeSpectrum.comap_comp {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {S' : Type u_1} [CommSemiring S'] (f : R →+* S) (g : S →+* S') :
      theorem PrimeSpectrum.comap_comp_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] {S' : Type u_1} [CommSemiring S'] (f : R →+* S) (g : S →+* S') (x : PrimeSpectrum S') :

      The comap of a surjective ring homomorphism is a closed embedding between the prime spectra.

      theorem PrimeSpectrum.comap_singleton_isClosed_of_isIntegral {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (x : PrimeSpectrum S) (hx : IsClosed {x}) :

      The prime spectrum of R × S is homeomorphic to the disjoint union of PrimeSpectrum R and PrimeSpectrum S.

      Equations
      Instances For

        basicOpen r is the open subset containing all prime ideals not containing r.

        Equations
        Instances For
          @[simp]
          theorem PrimeSpectrum.mem_basicOpen {R : Type u} [CommSemiring R] (f : R) (x : PrimeSpectrum R) :
          x PrimeSpectrum.basicOpen f fx.asIdeal
          @[simp]

          The specialization order #

          We endow PrimeSpectrum R with a partial order, where x ≤ y if and only if y ∈ closure {x}.

          Equations
          @[simp]
          theorem PrimeSpectrum.asIdeal_le_asIdeal {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) (y : PrimeSpectrum R) :
          x.asIdeal y.asIdeal x y
          @[simp]
          theorem PrimeSpectrum.asIdeal_lt_asIdeal {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) (y : PrimeSpectrum R) :
          x.asIdeal < y.asIdeal x < y
          @[simp]
          theorem PrimeSpectrum.nhdsOrderEmbedding_apply {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) :
          PrimeSpectrum.nhdsOrderEmbedding x = nhds x

          nhds as an order embedding.

          Equations
          Instances For
            Equations
            • =
            Equations
            Equations
            • PrimeSpectrum.instUnique = { default := , uniq := }

            If x specializes to y, then there is a natural map from the localization of y to the localization of x.

            Equations
            Instances For

              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.

              Equations
              Instances For

                Localizations at minimal primes have single-point prime spectra.

                Equations
                Instances For

                  Stacks: Lemma 00ES (3) 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.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The closed point in the prime spectrum of a local ring.

                    Equations
                    Instances For