app_injective_iff_stalkFunctor_map_injective

English

If a morphism f of sheaves is mono, then each stalk map (stalkFunctor x).map f is mono, and conversely, under suitable hypotheses, monomorphisms can be detected on stalks.

Русский

Если морфизм F ⟶ G между шефами моно, тогда каждая гомотетическая карта стэка моно; обратное верно при определённых условиях.

LaTeX

$$$\text{Mono}(f) \iff \forall x, \text{Mono}((stalkFunctor\ C\ x).map\,f.1)$$$

Lean4

theorem app_injective_iff_stalkFunctor_map_injective {F : Sheaf C X} {G : Presheaf C X} (f : F.1 ⟶ G) :
    (∀ x : X, Function.Injective ((stalkFunctor C x).map f)) ↔ ∀ U : Opens X, Function.Injective (f.app (op U)) :=
  ⟨fun h U => app_injective_of_stalkFunctor_map_injective f U fun x _ => h x,
    stalkFunctor_map_injective_of_app_injective⟩

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