English
Let F be a sheaf valued in a concrete category with forgetful functor reflecting isomorphisms and preserving limits. If two global sections over an open U have identical germs at every point of U, then the two sections are equal.
Русский
Пусть F — шеф над X в конкретной категории, забывающая функтор сохраняет изоморфизмы и пределы. Если две секции над открытым U совпадают по гёрмам в каждой точке U, то они равны.
LaTeX
$$$F: X\text{-Sheaf}, U\text{ открыто}, s,t\in F(U)\quad(\forall x\in U)\ germ_{U,x}(s)=germ_{U,x}(t)\Rightarrow s=t$$$
Lean4
/-- Let `F` be a sheaf valued in a concrete category, whose forgetful functor reflects isomorphisms,
preserves limits and filtered colimits. Then two sections who agree on every stalk must be equal.
-/
theorem section_ext (F : Sheaf C X) (U : Opens X) (s t : ToType (F.1.obj (op U)))
(h : ∀ (x : X) (hx : x ∈ U), F.presheaf.germ U x hx s = F.presheaf.germ U x hx t) : s = t := by
-- We use `germ_eq` and the axiom of choice, to pick for every point `x` a neighbourhood
-- `V x`, such that the restrictions of `s` and `t` to `V x` coincide.
choose V m i₁ i₂ heq using fun x : U =>
F.presheaf.germ_eq x.1 x.2 x.2 s t
(h x.1 x.2)
-- Since `F` is a sheaf, we can prove the equality locally, if we can show that these
-- neighborhoods form a cover of `U`.
apply F.eq_of_locally_eq' V U i₁
· intro x hxU
simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]
exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩
· intro x
rw [heq, Subsingleton.elim (i₁ x) (i₂ x)]
/-
Note that the analogous statement for surjectivity is false: Surjectivity on stalks does not
imply surjectivity of the components of a sheaf morphism. However it does imply that the morphism
is an epi, but this fact is not yet formalized.
-/
