English
Let F be a sheaf on a topological space X, and let V be an open subset of X. Suppose {U_i} is a family of open subsets with V contained in their union. If s and t are sections of F over V and, for every i, the restrictions of s and t to U_i coincide, then s = t.
Русский
Пусть F — оболочка на топологическопространстве X, пусть V — открытое подмножество X. Пусть семейство U_i покрывает V. Если две секции s и t над V имеют одинаковые ограничения на каждом U_i, то они совпадают на V.
LaTeX
$$$\forall s,t \in F(V),\ (\forall i, F.map (iUV i)^{op}\, s = F.map (iUV i)^{op}\, t) \Rightarrow s = t,$ где $V \le \iSup_i U_i$ (то есть покрытие), и $iUV i : U_i \to V$.$$
Lean4
/-- In this version of the lemma, the inclusion homs `iUV` can be specified directly by the user,
which can be more convenient in practice.
-/
theorem eq_of_locally_eq' (V : Opens X) (iUV : ∀ i : ι, U i ⟶ V) (hcover : V ≤ iSup U) (s t : ToType (F.1.obj (op V)))
(h : ∀ i, F.1.map (iUV i).op s = F.1.map (iUV i).op t) : s = t :=
by
have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)
suffices F.1.map (eqToHom V_eq_supr_U.symm).op s = F.1.map (eqToHom V_eq_supr_U.symm).op t by
convert congr_arg (F.1.map (eqToHom V_eq_supr_U).op) this <;>
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp, eqToHom_op, eqToHom_op, eqToHom_trans, eqToHom_refl,
F.1.map_id, ConcreteCategory.id_apply]
apply eq_of_locally_eq
intro i
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, ← F.1.map_comp]
exact h i
