fromSpecStalk_appTop — Mathlib

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 ..

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