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