Functoriality of the prime spectrum #

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

Main definitions #

PrimeSpectrum.comap: The induced map on prime spectra by a ring homomorphism. The proof that it is continuous is in Mathlib/RingTheory/Spectrum/Prime/Topology.lean.

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 {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) :

(comapEquiv e).symm = comapEquiv e.symm

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

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

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.

Documentation

Mathlib.RingTheory.Spectrum.Prime.RingHom

Functoriality of the prime spectrum #

Main definitions #