English
Let 𝒰 be an open cover of a scheme X. The three-fold glued transition maps satisfy a cocycle relation with the fst projection, i.e. the composed morphism along fst on the triple overlaps equals the fst projection on the first two factors.
Русский
Пусть 𝒰 — открытое покрытие схемы X. Утверждается коксивная (кокцикл) связь для трех последовательных переходов с проекцией fst: композиция связанных отображений для троичного пересечения эквивалентна проекции fst на первые два множителя.
LaTeX
$$$$ \_gluedCoverT'_{\mathcal{U}}(x,y,z) \;\circ\; \gluedCoverT'_{\mathcal{U}}(y,z,x) \;\circ\; \gluedCoverT'_{\mathcal{U}}(z,x,y) \;\circ\; \text{pullback.fst}_{(\mathcal{U}.f x),(\mathcal{U}.f y)} = \text{pullback.fst}_{(\mathcal{U}.f x),(\mathcal{U}.f y)}. $$$$
Lean4
theorem glued_cover_cocycle_fst (x y z : 𝒰.I₀) :
gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y ≫ pullback.fst _ _ = pullback.fst _ _ := by
apply pullback.hom_ext <;> simp
