English
If F → G is a natural transformation between presheaves and the component maps on all basis opens are injective, then the induced stalk map at every x is injective.
Русский
Пусть имеется натуральное преобразование F ⟶ G между прешефами, и компоненты на всех открытых из базиса инъективны; тогда стэковый отображатель в каждой точке x инъективен.
LaTeX
$$$\forall F,G: X\text{-Presheaf}, \forall \alpha: F\to G, (\forall U\in B,\mathrm{Injective}(\alpha.app(op\ U)))\Rightarrow\forall x:\,X,\mathrm{Injective}((stalkFunctor\ C\ x).map\alpha)$$$
Lean4
theorem stalkFunctor_map_injective_of_isBasis {F G : X.Presheaf C} {α : F ⟶ G}
(hα : ∀ U ∈ B, Function.Injective (α.app (op U))) (x : X) : Function.Injective ((stalkFunctor _ x).map α) :=
by
intro s t hst
obtain ⟨U₁, hxU₁, hU₁, s, rfl⟩ := germ_exist_of_isBasis hB _ x s
obtain ⟨U₂, hxU₂, hU₂, t, rfl⟩ := germ_exist_of_isBasis hB _ x t
rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply] at hst
obtain ⟨W, hxW, hW, iWU₁, iWU₂, heq⟩ := germ_eq_of_isBasis hB _ _ hxU₁ hxU₂ hst
simp only [← α.naturality_apply, (hα W hW).eq_iff] at heq
simpa [germ_res_apply'] using congr(F.germ W x hxW $heq)
