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.

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

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

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

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

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

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