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 ≃ 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) :
      (comapEquiv e).symm 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_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)

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