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
๐Ÿ”ธ coverage
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.

Instances For
    source
    ๐Ÿ”ธ coverage
    @[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.

    Instances For
      source
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[simp]
      theorem PrimeSpectrum.comap_id {R : Type u} [CommSemiring R] :
      comap (RingHom.id R) = fun (x : PrimeSpectrum R) => x
      source
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      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
      ๐Ÿ”ธ coverage
      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.

      Instances For
        source
        ๐Ÿ“ coverage
        @[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
        ๐Ÿ“ coverage
        @[simp]
        theorem PrimeSpectrum.comapEquiv_symm {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R โ‰ƒ+* S) :
        (comapEquiv e).symm = comapEquiv e.symm
        source
        ๐Ÿ”ธ coverage
        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.

        Instances For
          source
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          theorem PrimeSpectrum.sigmaToPi_injective {ฮน : Type u_3} (R : ฮน โ†’ Type u_2) [(i : ฮน) โ†’ CommSemiring (R i)] :
          Function.Injective (sigmaToPi R)
          source
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          theorem PrimeSpectrum.sigmaToPi_bijective {ฮน : Type u_3} (R : ฮน โ†’ Type u_4) [(i : ฮน) โ†’ CommRing (R i)] [Finite ฮน] :
          Function.Bijective (sigmaToPi R)
          source
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          @[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
          ๐Ÿ”ธ coverage
          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.

          Instances For
            source
            ๐Ÿ”ธ coverage
            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).

            Instances For
              source
              ๐Ÿ“ coverage
              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
              ๐Ÿ“ coverage
              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
              ๐Ÿ“ coverage
              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
              ๐Ÿ“ coverage
              @[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
              ๐Ÿ“ coverage
              theorem PrimeSpectrum.residueField_comap {R : Type u_1} [CommRing R] (I : PrimeSpectrum R) :
              Set.range (comap (algebraMap R I.asIdeal.ResidueField)) = {I}
              source
              ๐Ÿ“ coverage
              @[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
              ๐Ÿ“ coverage
              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
              ๐Ÿ“ coverage
              @[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.