stalkMap_injective_of_isAffine — Mathlib

English

If Y is affine and f: X ⟶ Y, then the stalk map f.stalkMap x is injective provided a germ-level hypothesis holds.

Русский

Если Y аффинна и f: X ⟶ Y, то отображение stalkMap f.x инъективно при условии на уровне жерла.

LaTeX

$$$(isAffineOpenTop Y).stalkMap_injective f x trivial h$$$

Lean4

theorem stalkMap_injective_of_isAffine {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] (x : X)
    (h : ∀ g, f.stalkMap x (Y.presheaf.Γgerm (f.base x) g) = 0 → Y.presheaf.Γgerm (f.base x) g = 0) :
    Function.Injective (f.stalkMap x) :=
  (isAffineOpen_top Y).stalkMap_injective f x trivial h

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