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

• PrimeSpectrum.comap f p = { asIdeal := Ideal.comap f p.asIdeal, isPrime := ⋯ }

@[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

@[simp]

theorem PrimeSpectrum.comap_id {R : Type u} [CommSemiring R] : comap (RingHom.id R) = fun (x : PrimeSpectrum R) => x

@[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

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)

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)

@[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)

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)

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

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

• PrimeSpectrum.comapEquiv e = { toFun := PrimeSpectrum.comap e.symm.toRingHom, invFun := PrimeSpectrum.comap e.toRingHom, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[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

@[simp]

theorem PrimeSpectrum.comapEquiv_symm {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : (comapEquiv e).symm = comapEquiv e.symm

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. This is always an open embedding, see PrimeSpectrum.isOpenEmbedding_sigmaToPi and a homeomorphism if ι is finite, see PrimeSpectrum.sigmaHomeoPi.

Equations

• PrimeSpectrum.sigmaToPi R ⟨i, p⟩ = PrimeSpectrum.comap (Pi.evalRingHom R i) p

@[simp]

theorem PrimeSpectrum.sigmaToPi_apply {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] (i : ι) (p : PrimeSpectrum (R i)) : sigmaToPi R ⟨i, p⟩ = comap (Pi.evalRingHom R i) p

@[deprecated PrimeSpectrum.sigmaToPi_apply (since := "2026-04-17")]

theorem PrimeSpectrum.coe_sigmaToPi_asIdeal {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] (i : ι) (p : PrimeSpectrum (R i)) : sigmaToPi R ⟨i, p⟩ = comap (Pi.evalRingHom R i) p

Alias of PrimeSpectrum.sigmaToPi_apply.

theorem PrimeSpectrum.sigmaToPi_injective {ι : Type u_3} (R : ι → Type u_2) [(i : ι) → CommSemiring (R i)] : Function.Injective (sigmaToPi R)

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.

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)

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

theorem PrimeSpectrum.sigmaToPi_bijective {ι : Type u_3} (R : ι → Type u_4) [(i : ι) → CommRing (R i)] [Finite ι] : Function.Bijective (sigmaToPi R)

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)

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)

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)

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.

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

• I.primeSpectrumQuotientOrderIsoZeroLocus = Ideal.primeSpectrumOrderIsoZeroLocusOfSurj (Ideal.Quotient.mk I) ⋯ ⋯

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.

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.

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)

theorem PrimeSpectrum.residueField_comap {R : Type u_1} [CommRing R] (I : PrimeSpectrum R) : Set.range (comap (algebraMap R I.asIdeal.ResidueField)) = {I}

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