English
Let X be a topological space, F a presheaf on X with values in a category C, and F' a sheaf on X. If two morphisms α, β: F → F' agree on every open from a basis B of X (i.e., ∀ i, α|_{B_i} = β|_{B_i}), then α = β.
Русский
Пусть X — топологическое пространство, F — прешейф над X в категорию C, F' — шейф над X. Пусть B = {U_i} образует базис открытых множеств. Тогда любые морфизмы α, β: F → F', совпадающие на каждом открытом U_i из B (то есть ∀ i, α|_{U_i} = β|_{U_i}), удовлетворяют α = β.
LaTeX
$$$\\forall \\alpha, \\beta : F \\to F',\\ (\\forall i, \\alpha|_{B_i} = \\beta|_{B_i}) \\Rightarrow \\alpha = \\beta$$$
Lean4
theorem hom_ext (h : Opens.IsBasis (Set.range B)) {α β : F ⟶ F'.1} (he : ∀ i, α.app (op (B i)) = β.app (op (B i))) :
α = β := by
apply (restrictHomEquivHom F F' h).symm.injective
ext i
exact he i.unop
