English
For any scheme X and point x, the morphism fromSpecStalk x can be rewritten via Spec.map and germ maps as a canonical morphism from Spec(X.presheaf.stalk x) to X.
Русский
Для схемы X и точки x отображение fromSpecStalk x эквивалентно через Spec.map и germ-карты каноническому морфизму.
LaTeX
$$ (X.fromSpecStalk x) = Spec.map ((ΓSpecIso (X.presheaf.stalk x)).inv ≫ (X.presheaf.germ ⊤ x trivial))$$
Lean4
theorem fromSpecStalk_appTop {x : X} :
(X.fromSpecStalk x).appTop =
X.presheaf.germ ⊤ x trivial ≫
(ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE le_top).op :=
fromSpecStalk_app ..