toSpecΓ_base — Mathlib

English

The canonical map X ⟶ Spec Γ(X, ⊤) is the unit of the Γ-Spec adjunction.

Русский

Каноническое отображение X ⟶ Spec(Γ(X, ⊤)) есть единица adjunction Γ-Spec.

LaTeX

$$def toSpecΓ (X : Scheme.{u}) : X ⟶ Spec Γ(X, ⊤) := ΓSpec.adjunction.unit.app X$$

Lean4

theorem toSpecΓ_base (X : Scheme.{u}) (x) :
    (Scheme.toSpecΓ X).base x = (Spec.map (X.presheaf.germ ⊤ x trivial)).base (IsLocalRing.closedPoint _) :=
  rfl

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