English
Let F be a presheaf on a topological space X, and let {U_i}_{i∈I} be a family of open subsets with union ⋃_i U_i. For each i, sf_i ∈ F(U_i) and s ∈ F(⋃_i U_i) be a candidate gluing of the sf_i. Then s is a gluing for the family (sf_i) iff for every i, the restriction of s to U_i equals sf_i.
Русский
Пусть F — предповерхность (presheaf) над топологическим пространством X, и пусть {U_i}_{i∈I} — семейство открытых подмножеств X с объединением ⋃_i U_i. Для каждого i дано sf_i ∈ F(U_i), а также s ∈ F(⋃_i U_i) — кандидат на склейку семейства sf_i. Тогда s является склейкой для (sf_i) тогда и только тогда, когда ограничение s на U_i равно sf_i для каждого i.
LaTeX
$$$\text{Gluing}(sf,s) \iff \forall i:\iota,\ s|_{U_i} = sf_i$$$
Lean4
/-- A section `s` is a gluing for a family of sections `sf` if it restricts to `sf i` on `U i`,
for all `i`
-/
def IsGluing (sf : ∀ i : ι, ToType (F.obj (op (U i)))) (s : ToType (F.obj (op (iSup U)))) : Prop :=
∀ i : ι, F.map (Opens.leSupr U i).op s = sf i
