English
Let f: X ⟶ Y be a morphism of schemes, U an affine open in Y, and x ∈ X with f.base x ∈ U. If a certain germ-level relation holds for all g ∈ Y.presheaf, then the induced map on stalks f.stalkMap x is injective.
Русский
Пусть f: X ⟶ Y — морфизм схема, U — аффинное открытое в Y, и x ∈ X так, что f.base x ∈ U. При выполнении определенного отношения на уровне гранок для всех g ∈ Y.presheaf соответствующее отображение на стадии stalk, f.stalkMap x, инъективно.
LaTeX
$$$\text{If } h: \forall g, f.stalkMap x (Y.presheaf.germ U (f.base x) h g)=0 \Rightarrow Y.presheaf.germ U (f.base x) h g = 0,\ then\ f.stalkMap x\ is\ injective$$$
Lean4
theorem stalkMap_injective (f : X ⟶ Y) {U : Opens Y} (hU : IsAffineOpen U) (x : X) (hx : f.base x ∈ U)
(h : ∀ g, f.stalkMap x (Y.presheaf.germ U (f.base x) hx g) = 0 → Y.presheaf.germ U (f.base x) hx g = 0) :
Function.Injective (f.stalkMap x) :=
by
letI := Y.presheaf.algebra_section_stalk ⟨f.base x, hx⟩
apply (hU.isLocalization_stalk ⟨f.base x, hx⟩).injective_of_map_algebraMap_zero
exact h
