sigmaToPi

Mathlib.RingTheory.Spectrum.Prime.RingHom

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.sigmaToPi

Lean4

/-- The canonical map from a disjoint union of prime spectra of commutative semirings to
the prime spectrum of the product semiring. -/
/- TODO: show this is always a topological embedding (even when ι is infinite)
and is a homeomorphism when ι is finite. -/

@[simps]
def sigmaToPi : (Σ i, PrimeSpectrum (R i)) → PrimeSpectrum (Π i, R i)
  | ⟨i, p⟩ => (Pi.evalRingHom R i).specComap p

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru