English
A variant of unique gluing where inclusion maps iUV are provided by the user; there exists a unique glued section on V that matches the prescribed data.
Русский
Вариант уникальной слепки, где включающие отображения iUV заданы пользователем; существует единственная слепка на V, совпадающая с данными sf.
LaTeX
$$$$\exists!\ s : F(U) \text{ such that } \forall i, F.map (iUV i)^{op} s = sf_i.$$$$
Lean4
@[ext]
theorem eq_of_locally_eq (s t : ToType (F.1.obj (op (iSup U))))
(h : ∀ i, F.1.map (Opens.leSupr U i).op s = F.1.map (Opens.leSupr U i).op t) : s = t :=
by
let sf : ∀ i : ι, ToType (F.1.obj (op (U i))) := fun i => F.1.map (Opens.leSupr U i).op s
have sf_compatible : IsCompatible _ U sf := by
intro i j
simp_rw [sf, ← ConcreteCategory.comp_apply, ← F.1.map_comp]
rfl
obtain ⟨gl, -, gl_uniq⟩ := F.existsUnique_gluing U sf sf_compatible
trans gl
· apply gl_uniq
intro i
rfl
· symm
apply gl_uniq
intro i
rw [← h]
