toΓSpecBase — Mathlib

English

The canonical (bundled) continuous map from the underlying topological space of X to Spec Γ(X) is defined by the global sections of X.

Русский

Каноническое непрерывное отображение из пространства X в спектр Γ(X) задаётся глобальными секциями X.

LaTeX

$$$X^{\text{toTop}} \to \operatorname{Spec}(\Gamma(X))$ is a continuous map.$$

Lean4

/-- The canonical (bundled) continuous map from the underlying topological
space of `X` to the prime spectrum of its global sections. -/
def toΓSpecBase : X.toTopCat ⟶ Spec.topObj (Γ.obj (op X)) :=
  TopCat.ofHom
    { toFun := X.toΓSpecFun
      continuous_toFun := X.toΓSpec_continuous }

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