Theorems · Definition · algebraic geometry

PrimeSpectrum.sigmaToPi

{ι : Type u_3} →
  (R : ι → Type u_2) →
    [inst : (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.

Defined in

Mathlib.RingTheory.Spectrum.Prime.RingHom

Cited by

10 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Quot.sound

Assumes

CommSemiring