English
If all component maps on opens are injective, then the stalk functor map induced by a morphism is injective.
Русский
Если все отображения на открытых множествах инъективны, отображение на стейки инъективно.
LaTeX
$$$$ (stalkFunctor C x).map f \text{ injective if } f.app(op U) \text{ injective for all } U.$$$$
Lean4
theorem stalkFunctor_map_injective_of_app_injective {F G : Presheaf C X} {f : F ⟶ G}
(h : ∀ U : Opens X, Function.Injective (f.app (op U))) (x : X) : Function.Injective ((stalkFunctor C x).map f) :=
fun s t hst => by
rcases germ_exist F x s with ⟨U₁, hxU₁, s, rfl⟩
rcases germ_exist F x t with ⟨U₂, hxU₂, t, rfl⟩
rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply] at hst
obtain ⟨W, hxW, iWU₁, iWU₂, heq⟩ := G.germ_eq x hxU₁ hxU₂ _ _ hst
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, ← f.naturality, ← f.naturality,
ConcreteCategory.comp_apply, ConcreteCategory.comp_apply] at heq
replace heq := h W heq
convert congr_arg (F.germ _ x hxW) heq using 1
exacts [(F.germ_res_apply iWU₁ x hxW s).symm, (F.germ_res_apply iWU₂ x hxW t).symm]
