stalk_mono_of_mono — Mathlib

English

If a morphism of presheaves is mono, then the corresponding stalk maps are mono for all x.

Русский

Если морфизм прешефов моно, то соответствующие карты стэков моно для всех x.

LaTeX

$$$\forall x,\ Mono((stalkFunctor\ C\ x).map f.1)$$$

Lean4

theorem stalk_mono_of_mono {F G : Sheaf C X} (f : F ⟶ G) [Mono f] : ∀ x, Mono <| (stalkFunctor C x).map f.1 := fun x =>
  Functor.map_mono (Sheaf.forget.{v} C X ⋙ stalkFunctor C x) f

Похожие утверждения