Spec_map_residue_apply — Mathlib

English

Applying the base map of Spec.map to a point s yields the closed point of the stalk.

Русский

Базовая карта Spec.map отправляет точку s в замкнутую точку локального стэка.

LaTeX

$$$$ (\operatorname{Spec.map}(X.\mathrm{residue}(x))).\mathrm{base}(s) = \mathrm{closedPoint}(X.\mathrm{presheaf.stalk}(x)). $$$$

Lean4

@[simp]
theorem Spec_map_residue_apply {X : Scheme.{u}} (x : X) (s : Spec (X.residueField x)) :
    (Spec.map (X.residue x)).base s = closedPoint (X.presheaf.stalk x) :=
  IsLocalRing.PrimeSpectrum.comap_residue _ s

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