English
The stalk functor preserves monomorphisms, i.e., applying the forgetful functor through the stalk preserves mono morphisms from presheaf to presheaf.
Русский
Сталк-функтор сохраняет моно-отображения, то есть моно-отображения сохраняются после применения забывающего функторa.
LaTeX
$$$\text{stalkFunctor}\ C\ x: (F\to G)\mapsto ((stalkFunctor\ C\ x).map\,f)$ preserves monos$$
Lean4
instance stalkFunctor_preserves_mono (x : X) :
Functor.PreservesMonomorphisms (Sheaf.forget.{v} C X ⋙ stalkFunctor C x) :=
⟨@fun _𝓐 _𝓑 f _ =>
ConcreteCategory.mono_of_injective _ <|
(app_injective_iff_stalkFunctor_map_injective f.1).mpr
(fun c =>
(ConcreteCategory.mono_iff_injective_of_preservesPullback (f.1.app (op c))).mp
((NatTrans.mono_iff_mono_app f.1).mp (CategoryTheory.presheaf_mono_of_mono ..) <| op c))
x⟩
