English
Given a presheaf F on a topological category X and a family of opens U_i with sections sf_i ∈ F(U_i), there is a canonical way to assign to every index i of the pairwise diagram a section over the corresponding open, namely sf_i on the singleton node and the restriction to the intersection on the pair node.
Русский
Дано прешейф F на топологическом объекте X и семейство открытых множеств U_i с секциями sf_i ∈ F(U_i); существует каноническое продолжение к парным пересечениям: на узлом пары узлы дают ограничение, а на узлу одиночности — сами sf_i.
LaTeX
$$$$\text{Given a presheaf }F\text{ and opens }U_i,\quad sf\!:\! \forall i, F(op(U_i))\to \\text{objPairwiseOfFamily}(sf).$$
-\text{If } i=\\langle\\text{Pairwise.single } i\\rangle: \text{ value }= sf_i,
-\text{If } i=\\langle\\text{Pairwise.pair } i j\\rangle: \text{ value }= F.map (infLELeft (U_i) (U_j)).op (sf_i).$$$$
Lean4
/-- Given sections over a family of open sets, extend it to include
sections over pairwise intersections of the open sets. -/
def objPairwiseOfFamily (sf : ∀ i, F.obj (op (U i))) : ∀ i, ((Pairwise.diagram U).op ⋙ F).obj i
| ⟨Pairwise.single i⟩ => sf i
| ⟨Pairwise.pair i j⟩ => F.map (infLELeft (U i) (U j)).op (sf i)
