Documentation

Mathlib.RingTheory.Spectrum.Prime.RingHom

Functoriality of the prime spectrum #

In this file we define the induced map on prime spectra induced by a ring homomorphism.

Main definitions #

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

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

Equations
    Instances For
      source
      theorem PrimeSpectrum.preimage_specComap_zeroLocus_aux {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Set R) :
      f.specComap ⁻¹' zeroLocus s = zeroLocus (⇑f '' s)
      source
      @[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
      source
      @[simp]
      theorem PrimeSpectrum.specComap_id {R : Type u} [CommSemiring R] :
      (RingHom.id R).specComap = fun (x : PrimeSpectrum R) => x
      source
      @[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
      source
      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)
      source
      @[simp]
      theorem PrimeSpectrum.preimage_specComap_zeroLocus {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Set R) :
      f.specComap ⁻¹' zeroLocus s = zeroLocus (⇑f '' s)
      source
      theorem PrimeSpectrum.specComap_injective_of_surjective {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
      Function.Injective f.specComap
      source
      def PrimeSpectrum.comapEquiv {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) :
      PrimeSpectrum R ≃o PrimeSpectrum S

      RingHom.specComap of an isomorphism of rings as an equivalence of their prime spectra.

      Equations
        Instances For
          source
          @[simp]
          theorem PrimeSpectrum.comapEquiv_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) (a✝ : PrimeSpectrum R) :
          (comapEquiv e) a✝ = e.symm.toRingHom.specComap a✝
          source
          @[simp]
          theorem PrimeSpectrum.comapEquiv_symm_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) (a✝ : PrimeSpectrum S) :
          (RelIso.symm (comapEquiv e)) a✝ = e.toRingHom.specComap a✝
          source
          def PrimeSpectrum.sigmaToPi {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] :
          (i : ι) × PrimeSpectrum (R i) → PrimeSpectrum ((i : ι) → R i)

          The canonical map from a disjoint union of prime spectra of commutative semirings to the prime spectrum of the product semiring.

          Equations
            Instances For
              source
              @[simp]
              theorem PrimeSpectrum.sigmaToPi_asIdeal {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] (a✝ : (i : ι) × PrimeSpectrum (R i)) :
              (sigmaToPi R a✝).asIdeal = Ideal.comap (Pi.evalRingHom R a✝.fst) a✝.snd.asIdeal
              source
              theorem PrimeSpectrum.sigmaToPi_injective {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] :
              Function.Injective (sigmaToPi R)
              source
              theorem PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] [Infinite ι] [∀ (i : ι), Nontrivial (R i)] :
              ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

              An infinite product of nontrivial commutative semirings has a maximal ideal outside of the range of sigmaToPi, i.e. is not of the form πᵢ⁻¹(𝔭) for some prime 𝔭 ⊂ R i, where πᵢ : (Π i, R i) →+* R i is the projection. For a complete description of all prime ideals, see https://math.stackexchange.com/a/1563190.

              source
              @[deprecated PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite (since := "2025-05-24")]
              theorem PrimeSpectrum.exists_maximal_nmem_range_sigmaToPi_of_infinite {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] [Infinite ι] [∀ (i : ι), Nontrivial (R i)] :
              ∃ (I : Ideal ((i : ι) → R i)) (x : I.IsMaximal), { asIdeal := I, isPrime := ⋯ } ∉ Set.range (sigmaToPi R)

              Alias of PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite.

              An infinite product of nontrivial commutative semirings has a maximal ideal outside of the range of sigmaToPi, i.e. is not of the form πᵢ⁻¹(𝔭) for some prime 𝔭 ⊂ R i, where πᵢ : (Π i, R i) →+* R i is the projection. For a complete description of all prime ideals, see https://math.stackexchange.com/a/1563190.

              source
              theorem PrimeSpectrum.sigmaToPi_not_surjective_of_infinite {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] [Infinite ι] [∀ (i : ι), Nontrivial (R i)] :
              ¬Function.Surjective (sigmaToPi R)
              source
              theorem PrimeSpectrum.exists_comap_evalRingHom_eq {ι : Type u_3} {R : ι → Type u_4} [(i : ι) → CommRing (R i)] [Finite ι] (p : PrimeSpectrum ((i : ι) → R i)) :
              ∃ (i : ι) (q : PrimeSpectrum (R i)), (Pi.evalRingHom R i).specComap q = p
              source
              theorem PrimeSpectrum.sigmaToPi_bijective {ι : Type u_3} (R : ι → Type u_4) [(i : ι) → CommRing (R i)] [Finite ι] :
              Function.Bijective (sigmaToPi R)
              source
              theorem PrimeSpectrum.iUnion_range_specComap_comp_evalRingHom {ι : Type u_3} {R : ι → Type u_4} [(i : ι) → CommRing (R i)] [Finite ι] {S : Type u_5} [CommRing S] (f : S →+* (i : ι) → R i) :
              ⋃ (i : ι), Set.range ((Pi.evalRingHom R i).comp f).specComap = Set.range f.specComap
              source
              theorem image_specComap_zeroLocus_eq_zeroLocus_comap {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (I : Ideal S) :
              f.specComap '' PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)
              source
              theorem range_specComap_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
              Set.range f.specComap = PrimeSpectrum.zeroLocus ↑(RingHom.ker f)
              source
              noncomputable def Ideal.primeSpectrumOrderIsoZeroLocusOfSurj {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) {I : Ideal R} (hI : RingHom.ker f = I) :
              PrimeSpectrum S ≃o ↑(PrimeSpectrum.zeroLocus ↑I)

              Let f : R →+* S be a surjective ring homomorphism, then Spec S is order-isomorphic to Z(I) where I = ker f.

              Equations
                Instances For
                  source
                  noncomputable def Ideal.primeSpectrumQuotientOrderIsoZeroLocus {R : Type u} [CommRing R] (I : Ideal R) :
                  PrimeSpectrum (R ⧸ I) ≃o ↑(PrimeSpectrum.zeroLocus ↑I)

                  Spec (R / I) is order-isomorphic to Z(I).

                  Equations
                    Instances For
                      source
                      theorem PrimeSpectrum.mem_range_comap_iff {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) {p : PrimeSpectrum R} :
                      p ∈ Set.range f.specComap ↔ Ideal.comap f (Ideal.map f p.asIdeal) = p.asIdeal

                      p is in the image of Spec S → Spec R if and only if p extended to S and restricted back to R is p.

                      source
                      theorem PrimeSpectrum.nontrivial_iff_mem_rangeComap {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] [Algebra R S] (p : PrimeSpectrum R) :
                      Nontrivial (TensorProduct R p.asIdeal.ResidueField S) ↔ p ∈ Set.range (algebraMap R S).specComap

                      A prime p is in the range of Spec S → Spec R if the fiber over p is nontrivial.

                      source
                      theorem PrimeSpectrum.residueField_specComap {R : Type u_1} [CommRing R] (I : PrimeSpectrum R) :
                      Set.range (algebraMap R I.asIdeal.ResidueField).specComap = {I}