English
For a compatible family sf of sections over opens U_i, a section s over the union glues sf exactly when each projection to the i-th component matches the corresponding pairwise extension.
Русский
Для совместимой семейства секций sf над открытыми множествами U_i существующая секция s над объединением сшивает sf тогда и только тогда, когда каждая проекция на i-ю компоненту совпадает с соответствующим парным расширением.
LaTeX
$$$$\text{IsGluing } F\, U\, sf\, s \;\Longleftrightarrow\; \forall i,\ (F.mapCone (Pairwise.cocone U).op).\pi_{app i}\, s = objPairwiseOfFamily\ sf\ i.$$$$
Lean4
/-- Given a compatible family of sections over open sets, extend it to a
section of the functor `(Pairwise.diagram U).op ⋙ F`. -/
def sectionPairwise {sf} (h : IsCompatible F U sf) : ((Pairwise.diagram U).op ⋙ F).sections :=
by
refine ⟨objPairwiseOfFamily sf, ?_⟩
let G := (Pairwise.diagram U).op ⋙ F
rintro (i | ⟨i, j⟩) (i' | ⟨i', j'⟩) (_ | _ | _ | _)
· exact congr_fun (G.map_id <| op <| Pairwise.single i) _
· rfl
· exact (h i' i).symm
· exact congr_fun (G.map_id <| op <| Pairwise.pair i j) _
