English
Let F be a presheaf on X with values in C, and suppose we have a family s_i ∈ F(U_i) indexed by i ∈ I. This family is compatible if for every i, j, the restrictions of s_i and s_j to the overlap U_i ∩ U_j agree: res_{U_i}^{U_i∩U_j}(s_i) = res_{U_j}^{U_i∩U_j}(s_j).
Русский
Пусть F — прешейф на X в C. Пусть дано семейство секций s_i ∈ F(U_i) над открытыми множествами U_i, индексируемое i ∈ I. Это семейство совместимо, если для любых i, j их ограничения на пересечение U_i ∩ U_j совпадают: res_{U_i}^{U_i∩U_j}(s_i) = res_{U_j}^{U_i∩U_j}(s_j).
LaTeX
$$$\\forall i,j,\\ \\operatorname{Res}_{U_i \cap U_j}^{U_i}(s_i) = \\operatorname{Res}_{U_i \cap U_j}^{U_j}(s_j)$$$
Lean4
/-- A family of sections `sf` is compatible, if the restrictions of `sf i` and `sf j` to `U i ⊓ U j`
agree, for all `i` and `j`
-/
def IsCompatible (sf : ∀ i : ι, ToType (F.obj (op (U i)))) : Prop :=
∀ i j : ι, F.map (infLELeft (U i) (U j)).op (sf i) = F.map (infLERight (U i) (U j)).op (sf j)
