Documentation

Mathlib.RingTheory.PrimeSpectrum

Prime spectrum of a commutative (semi)ring as a type #

The prime spectrum of a commutative (semi)ring is the type of all prime ideals.

For the Zariski topology, see AlgebraicGeometry.PrimeSpectrum.Basic.

(It is also naturally endowed with a sheaf of rings, which is constructed in AlgebraicGeometry.StructureSheaf.)

Main definitions #

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).

theorem PrimeSpectrum.ext {R : Type u} :
∀ {inst : CommSemiring R} {x y : PrimeSpectrum R}, x.asIdeal = y.asIdealx = y
theorem PrimeSpectrum.ext_iff {R : Type u} :
∀ {inst : CommSemiring R} {x y : PrimeSpectrum R}, x = y x.asIdeal = y.asIdeal
structure PrimeSpectrum (R : Type u) [CommSemiring R] :

The prime spectrum of a commutative (semi)ring R is the type of all prime ideals of R.

It is naturally endowed with a topology (the Zariski topology), and a sheaf of commutative rings (see AlgebraicGeometry.StructureSheaf). It is a fundamental building block in algebraic geometry.

  • asIdeal : Ideal R
  • isPrime : self.asIdeal.IsPrime
Instances For
    theorem PrimeSpectrum.isPrime {R : Type u} [CommSemiring R] (self : PrimeSpectrum R) :
    self.asIdeal.IsPrime
    @[deprecated PrimeSpectrum.isPrime]
    theorem PrimeSpectrum.IsPrime {R : Type u} [CommSemiring R] (self : PrimeSpectrum R) :
    self.asIdeal.IsPrime

    Alias of PrimeSpectrum.isPrime.

    The prime spectrum of the zero ring is empty.

    Equations
    • =

    The map from the direct sum of prime spectra to the prime spectrum of a direct product.

    Equations
    Instances For

      The prime spectrum of R × S is in bijection with the disjoint unions of the prime spectrum of R and the prime spectrum of S.

      Equations
      Instances For
        @[simp]
        theorem PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (x : PrimeSpectrum R) :
        ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = x.asIdeal.prod
        @[simp]
        theorem PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (x : PrimeSpectrum S) :
        ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = .prod x.asIdeal

        The zero locus of a set s of elements of a commutative (semi)ring R is the set of all prime ideals of the ring that contain the set s.

        An element f of R can be thought of as a dependent function on the prime spectrum of R. At a point x (a prime ideal) the function (i.e., element) f takes values in the quotient ring R modulo the prime ideal x. In this manner, zeroLocus s is exactly the subset of PrimeSpectrum R where all "functions" in s vanish simultaneously.

        Equations
        Instances For
          @[simp]
          theorem PrimeSpectrum.mem_zeroLocus {R : Type u} [CommSemiring R] (x : PrimeSpectrum R) (s : Set R) :
          x PrimeSpectrum.zeroLocus s s x.asIdeal

          The vanishing ideal of a set t of points of the prime spectrum of a commutative ring R is the intersection of all the prime ideals in the set t.

          An element f of R can be thought of as a dependent function on the prime spectrum of R. At a point x (a prime ideal) the function (i.e., element) f takes values in the quotient ring R modulo the prime ideal x. In this manner, vanishingIdeal t is exactly the ideal of R consisting of all "functions" that vanish on all of t.

          Equations
          Instances For
            theorem PrimeSpectrum.coe_vanishingIdeal {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) :
            (PrimeSpectrum.vanishingIdeal t) = {f : R | xt, f x.asIdeal}
            theorem PrimeSpectrum.mem_vanishingIdeal {R : Type u} [CommSemiring R] (t : Set (PrimeSpectrum R)) (f : R) :
            f PrimeSpectrum.vanishingIdeal t xt, f x.asIdeal

            zeroLocus and vanishingIdeal form a galois connection.

            theorem PrimeSpectrum.zeroLocus_iSup {R : Type u} [CommSemiring R] {ι : Sort u_1} (I : ιIdeal R) :
            PrimeSpectrum.zeroLocus (⨆ (i : ι), I i) = ⋂ (i : ι), PrimeSpectrum.zeroLocus (I i)
            theorem PrimeSpectrum.zeroLocus_iUnion {R : Type u} [CommSemiring R] {ι : Sort u_1} (s : ιSet R) :
            PrimeSpectrum.zeroLocus (⋃ (i : ι), s i) = ⋂ (i : ι), PrimeSpectrum.zeroLocus (s i)
            theorem PrimeSpectrum.zeroLocus_iUnion₂ {R : Type u} [CommSemiring R] {ι : Sort u_1} {κ : ιSort u_2} (s : (i : ι) → κ iSet R) :
            PrimeSpectrum.zeroLocus (⋃ (i : ι), ⋃ (j : κ i), s i j) = ⋂ (i : ι), ⋂ (j : κ i), PrimeSpectrum.zeroLocus (s i j)
            theorem PrimeSpectrum.zeroLocus_bUnion {R : Type u} [CommSemiring R] (s : Set (Set R)) :
            PrimeSpectrum.zeroLocus (⋃ s's, s') = s's, PrimeSpectrum.zeroLocus s'
            theorem PrimeSpectrum.vanishingIdeal_iUnion {R : Type u} [CommSemiring R] {ι : Sort u_1} (t : ιSet (PrimeSpectrum R)) :
            PrimeSpectrum.vanishingIdeal (⋃ (i : ι), t i) = ⨅ (i : ι), PrimeSpectrum.vanishingIdeal (t i)
            @[simp]
            theorem PrimeSpectrum.zeroLocus_pow {R : Type u} [CommSemiring R] (I : Ideal R) {n : } (hn : n 0) :

            The specialization order #

            We endow PrimeSpectrum R with a partial order induced from the ideal lattice. This is exactly the specialization order. See the corresponding section at Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.

            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
            Equations
            Equations
            • PrimeSpectrum.instUnique = { default := , uniq := }
            theorem PrimeSpectrum.exists_primeSpectrum_prod_le (R : Type u) [CommRing R] [IsNoetherianRing R] (I : Ideal R) :
            ∃ (Z : Multiset (PrimeSpectrum R)), (Multiset.map PrimeSpectrum.asIdeal Z).prod I

            In a noetherian ring, every ideal contains a product of prime ideals ([samuel, § 3.3, Lemma 3])

            theorem PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A] (h_fA : ¬IsField A) {I : Ideal A} (h_nzI : I ) :
            ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map PrimeSpectrum.asIdeal Z).prod I (Multiset.map PrimeSpectrum.asIdeal Z).prod

            In a noetherian integral domain which is not a field, every non-zero ideal contains a non-zero product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as product or prime ideals ([samuel, § 3.3, Lemma 3])

            @[reducible, inline]
            abbrev RingHom.specComap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) :

            The pullback of an element of PrimeSpectrum S along a ring homomorphism f : R →+* S. The bundled continuous version is PrimeSpectrum.comap.

            Equations
            • f.specComap y = { asIdeal := Ideal.comap f y.asIdeal, isPrime := }
            Instances For
              @[simp]
              theorem PrimeSpectrum.specComap_asIdeal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (y : PrimeSpectrum S) :
              (f.specComap y).asIdeal = Ideal.comap f y.asIdeal
              @[simp]
              theorem PrimeSpectrum.specComap_id {R : Type u} [CommSemiring R] :
              (RingHom.id R).specComap = fun (x : PrimeSpectrum R) => x
              @[simp]
              theorem PrimeSpectrum.specComap_comp {R : Type u} {S : Type v} {S' : Type u_1} [CommSemiring R] [CommSemiring S] [CommSemiring S'] (f : R →+* S) (g : S →+* S') :
              (g.comp f).specComap = f.specComap g.specComap
              theorem PrimeSpectrum.specComap_comp_apply {R : Type u} {S : Type v} {S' : Type u_1} [CommSemiring R] [CommSemiring S] [CommSemiring S'] (f : R →+* S) (g : S →+* S') (x : PrimeSpectrum S') :
              (g.comp f).specComap x = f.specComap (g.specComap x)
              theorem PrimeSpectrum.localization_specComap_range {R : Type u} (S : Type v) [CommSemiring R] [CommSemiring S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
              Set.range (algebraMap R S).specComap = {p : PrimeSpectrum R | Disjoint M p.asIdeal}