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
def PrimeSpectrum.comap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (p : 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
    @[deprecated PrimeSpectrum.comap (since := "2025-12-10")]
    def RingHom.specComap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (p : PrimeSpectrum S) :
    PrimeSpectrum R

    Alias of PrimeSpectrum.comap.

    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
      @[simp]
      theorem PrimeSpectrum.comap_asIdeal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (y : PrimeSpectrum S) :
      (comap f y).asIdeal = Ideal.comap f y.asIdeal
      source
      @[deprecated PrimeSpectrum.comap_asIdeal (since := "2025-12-10")]
      theorem PrimeSpectrum.specComap_asIdeal {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (y : PrimeSpectrum S) :
      (comap f y).asIdeal = Ideal.comap f y.asIdeal

      Alias of PrimeSpectrum.comap_asIdeal.

      source
      @[simp]
      theorem PrimeSpectrum.comap_id {R : Type u} [CommSemiring R] :
      comap (RingHom.id R) = fun (x : PrimeSpectrum R) => x
      source
      @[deprecated PrimeSpectrum.comap_id (since := "2025-12-10")]
      theorem PrimeSpectrum.specComap_id {R : Type u} [CommSemiring R] :
      comap (RingHom.id R) = fun (x : PrimeSpectrum R) => x

      Alias of PrimeSpectrum.comap_id.

      source
      @[simp]
      theorem PrimeSpectrum.comap_comp {R : Type u} {S : Type v} {S' : Type u_1} [CommSemiring R] [CommSemiring S] [CommSemiring S'] (f : R →+* S) (g : S →+* S') :
      comap (g.comp f) = comap f ∘ comap g
      source
      @[deprecated PrimeSpectrum.comap_comp (since := "2025-12-10")]
      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') :
      comap (g.comp f) = comap f ∘ comap g

      Alias of PrimeSpectrum.comap_comp.

      source
      theorem PrimeSpectrum.comap_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') :
      comap (g.comp f) x = comap f (comap g x)
      source
      @[deprecated PrimeSpectrum.comap_comp_apply (since := "2025-12-10")]
      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') :
      comap (g.comp f) x = comap f (comap g x)

      Alias of PrimeSpectrum.comap_comp_apply.

      source
      theorem PrimeSpectrum.preimage_comap_zeroLocus_aux {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Set R) :
      comap f ⁻¹' zeroLocus s = zeroLocus (⇑f '' s)
      source
      @[simp]
      theorem PrimeSpectrum.preimage_comap_zeroLocus {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Set R) :
      comap f ⁻¹' zeroLocus s = zeroLocus (⇑f '' s)
      source
      @[deprecated PrimeSpectrum.preimage_comap_zeroLocus (since := "2025-12-10")]
      theorem PrimeSpectrum.preimage_specComap_zeroLocus {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (s : Set R) :
      comap f ⁻¹' zeroLocus s = zeroLocus (⇑f '' s)

      Alias of PrimeSpectrum.preimage_comap_zeroLocus.

      source
      theorem PrimeSpectrum.comap_injective_of_surjective {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
      Function.Injective (comap f)
      source
      @[deprecated PrimeSpectrum.comap_injective_of_surjective (since := "2025-12-10")]
      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 (comap f)

      Alias of PrimeSpectrum.comap_injective_of_surjective.

      source
      instance PrimeSpectrum.instLiesOverAsIdealComapAlgebraMap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] [Algebra R S] (p : PrimeSpectrum S) :
      p.asIdeal.LiesOver (comap (algebraMap R S) p).asIdeal
      source
      def PrimeSpectrum.comapEquiv {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) :
      PrimeSpectrum R ≃o PrimeSpectrum S

      RingHom.comap 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) (p : PrimeSpectrum R) :
        (comapEquiv e) p = comap e.symm.toRingHom p
        source
        @[simp]
        theorem PrimeSpectrum.comapEquiv_symm_apply {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) (p : PrimeSpectrum S) :
        (RelIso.symm (comapEquiv e)) p = comap e.toRingHom p
        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)), comap (Pi.evalRingHom R i) 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_comap_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 (comap ((Pi.evalRingHom R i).comp f)) = Set.range (comap f)
          source
          @[deprecated PrimeSpectrum.iUnion_range_comap_comp_evalRingHom (since := "2025-12-11")]
          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 (comap ((Pi.evalRingHom R i).comp f)) = Set.range (comap f)

          Alias of PrimeSpectrum.iUnion_range_comap_comp_evalRingHom.

          source
          theorem image_comap_zeroLocus_eq_zeroLocus_comap {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (I : Ideal S) :
          PrimeSpectrum.comap f '' PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)
          source
          @[deprecated image_comap_zeroLocus_eq_zeroLocus_comap (since := "2025-12-10")]
          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) :
          PrimeSpectrum.comap f '' PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)

          Alias of image_comap_zeroLocus_eq_zeroLocus_comap.

          source
          theorem range_comap_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
          Set.range (PrimeSpectrum.comap f) = PrimeSpectrum.zeroLocus ↑(RingHom.ker f)
          source
          @[deprecated range_comap_of_surjective (since := "2025-12-10")]
          theorem range_specComap_of_surjective {R : Type u} (S : Type v) [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
          Set.range (PrimeSpectrum.comap f) = PrimeSpectrum.zeroLocus ↑(RingHom.ker f)

          Alias of range_comap_of_surjective.

          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
          • One or more equations did not get rendered due to their size.
          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 (comap f) ↔ 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 (comap (algebraMap R S))

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

              source
              theorem RingHom.strictMono_comap_of_surjective {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) :
              StrictMono (PrimeSpectrum.comap f)
              source
              @[deprecated RingHom.strictMono_comap_of_surjective (since := "2025-12-10")]
              theorem RingHom.strictMono_specComap_of_surjective {R : Type u} [CommRing R] {S : Type u_1} [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) :
              StrictMono (PrimeSpectrum.comap f)

              Alias of RingHom.strictMono_comap_of_surjective.

              source
              theorem PrimeSpectrum.residueField_comap {R : Type u_1} [CommRing R] (I : PrimeSpectrum R) :
              Set.range (comap (algebraMap R I.asIdeal.ResidueField)) = {I}
              source
              @[deprecated PrimeSpectrum.residueField_comap (since := "2025-12-10")]
              theorem PrimeSpectrum.residueField_specComap {R : Type u_1} [CommRing R] (I : PrimeSpectrum R) :
              Set.range (comap (algebraMap R I.asIdeal.ResidueField)) = {I}

              Alias of PrimeSpectrum.residueField_comap.

              source
              theorem IsLocalHom.of_comap_surjective {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Surjective (PrimeSpectrum.comap f)) :
              IsLocalHom f
              source
              @[deprecated IsLocalHom.of_comap_surjective (since := "2025-12-10")]
              theorem IsLocalHom.of_specComap_surjective {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (hf : Function.Surjective (PrimeSpectrum.comap f)) :
              IsLocalHom f

              Alias of IsLocalHom.of_comap_surjective.