toPrimeSpectrum_range — Mathlib

English

Let R be a commutative ring. The image of the map toPrimeSpectrum is exactly the set of prime spectrum points that are closed as singletons in the Zariski topology.

Русский

Пусть R — коммутативное кольцо. Образ отображения toPrimeSpectrum равен множеству точек спектра простых, которые являются замкнутыми одиночками в зариcковской топологии.

LaTeX

$$$\\\\operatorname{range}(\\\\operatorname{toPrimeSpectrum}) = \\\\{ x \\\\in \\\\operatorname{PrimeSpectrum}(R) \\\\mid \\\\operatorname{IsClosed}(\\\\{x\\\\}) \\\}$$$

Lean4

theorem toPrimeSpectrum_range : Set.range (@toPrimeSpectrum R _) = {x | IsClosed ({ x } : Set <| PrimeSpectrum R)} :=
  by
  simp only [isClosed_singleton_iff_isMaximal]
  ext ⟨x, _⟩
  exact ⟨fun ⟨y, hy⟩ => hy ▸ y.isMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩

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