English
Conversely, if all stalk maps are mono and the forgetful functor reflects isomorphisms, then the presheaf morphism is mono.
Русский
Обратно, если все карты стэков моно и забывающая функтор отражает изоморфизмы, тогда морфизм прешефа моно.
LaTeX
$$$\text{Mono}(f) \iff \forall x, \text{Mono}((stalkFunctor\ C\ x).map f.1)$$$
Lean4
theorem mono_of_stalk_mono {F G : Sheaf C X} (f : F ⟶ G) [∀ x, Mono <| (stalkFunctor C x).map f.1] : Mono f :=
(Sheaf.Hom.mono_iff_presheaf_mono _ _ _).mpr <|
(NatTrans.mono_iff_mono_app _).mpr fun U =>
(ConcreteCategory.mono_iff_injective_of_preservesPullback _).mpr <|
app_injective_of_stalkFunctor_map_injective f.1 U.unop fun _x _hx =>
(ConcreteCategory.mono_iff_injective_of_preservesPullback ((stalkFunctor C _).map f.val)).mp <| inferInstance
