app_injective_of_stalkFunctor_map_injective

English

If for a morphism f: F ⟶ G of sheaves all stalk maps are injective, then the corresponding map on sections f.app(U) is injective for each open U.

Русский

Если все отображения стэков для f инъективны, то отображение f.app(U) на секциях над любом открытом U инъективно.

LaTeX

$$$\forall U\ Opens(X), \mathrm{Injective}(f.app(op\ U)) \,\leftarrow\, \forall x\in X, \mathrm{Injective}(((stalkFunctor\ C\ x).map\,f.1) )$$$

Lean4

theorem app_injective_of_stalkFunctor_map_injective {F : Sheaf C X} {G : Presheaf C X} (f : F.1 ⟶ G) (U : Opens X)
    (h : ∀ x ∈ U, Function.Injective ((stalkFunctor C x).map f)) : Function.Injective (f.app (op U)) := fun s t hst =>
  section_ext F _ _ _ fun x hx => h x hx <| by rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply, hst]

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