English
If a morphism f between sheafed spaces has an injective base map and each stalk map is epi, then f is mono.
Русский
Если морфизм между расслоенными пространствами имеет инъективную базовую карту и каждый stalkMap эпиморфизм, тогда f моно
LaTeX
$$$\forall f:X\to Y,\;\mathrm{Injective}(f.base)\land (\forall x,\mathrm{Epi}(f.stalkMap\,x))\Rightarrow \mathrm{Mono}(f)$$$
Lean4
theorem hom_stalk_ext {X Y : SheafedSpace C} (f g : X ⟶ Y) (h : f.base = g.base)
(h' : ∀ x, f.stalkMap x = (Y.presheaf.stalkCongr (h ▸ rfl)).hom ≫ g.stalkMap x) : f = g :=
by
obtain ⟨f, fc⟩ := f
obtain ⟨g, gc⟩ := g
obtain rfl : f = g := h
congr
ext U s
refine section_ext X.sheaf _ _ _ fun x hx ↦ show X.presheaf.germ _ x _ _ = X.presheaf.germ _ x _ _ from ?_
erw [← PresheafedSpace.stalkMap_germ_apply ⟨f, fc⟩, ← PresheafedSpace.stalkMap_germ_apply ⟨f, gc⟩]
simp [h']
