toΓSpec_continuous — Mathlib

English

For any locally ringed space X, the canonical map from the underlying topological space of X to the prime spectrum of the global sections Γ(X) is continuous.

Русский

Пусть X — локально кольцевое пространство; каноническая карта из множества точек X в спектр Гегlobal секций Γ(X) непрерывна.

LaTeX

$$$\forall X:\, \text{LocallyRingedSpace},\; \text{Continuous}(X.to\Gamma SpecFun).$$$

Lean4

/-- `toΓSpecFun` is continuous. -/
theorem toΓSpec_continuous : Continuous X.toΓSpecFun :=
  by
  rw [isTopologicalBasis_basic_opens.continuous_iff]
  rintro _ ⟨r, rfl⟩
  rw [X.toΓSpec_preimage_basicOpen_eq r]
  exact (X.toRingedSpace.basicOpen r).2

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