toΓSpecFun — Mathlib

English

The preimage of a basic open under the unit X → Spec Γ(X) is exactly the basic open in X defined by the same element.

Русский

Преобраз предобраза базового открытого по единице X → Spec Γ(X) совпадает с базовым открытым в X, заданным тем же элементом.

LaTeX

$$$X.toΓSpecFun^{-1}(.{\text{basicOpen}}(r)) = {\text{basicOpen}}_X(r)$$$

Lean4

/-- The canonical map from the underlying set to the prime spectrum of `Γ(X)`. -/
def toΓSpecFun : X → PrimeSpectrum (Γ.obj (op X)) := fun x =>
  comap (X.presheaf.Γgerm x).hom (IsLocalRing.closedPoint (X.presheaf.stalk x))

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