glued_cover_cocycle — Mathlib

English

Let 𝒰 be an open cover of X. The triple composition of gluedCoverT' equals the identity on the corresponding pullback, i.e. the cocycle condition yields an equality to the identity morphism.

Русский

Пусть 𝒰 — открытое покрытие X. Тройная композиция gluedCoverT' равна единице на соответствующем pullback; cocycle-условие приводит к равенству с тождественным отображением.

LaTeX

$$$$ \gluedCoverT'_{\mathcal{U}}(x,y,z) \circ \gluedCoverT'_{\mathcal{U}}(y,z,x) \circ \gluedCoverT'_{\mathcal{U}}(z,x,y) = \mathrm{Id}. $$$$

Lean4

theorem glued_cover_cocycle (x y z : 𝒰.I₀) : gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y = 𝟙 _ :=
  by
  apply pullback.hom_ext <;> simp_rw [Category.id_comp, Category.assoc]
  · apply glued_cover_cocycle_fst
  · apply glued_cover_cocycle_snd

Похожие утверждения