English
Full cocycle relation for the triple t' across i, j, k with all fst/fst/snd interactions; the composition equals the identity.
Русский
Полное кокосовое тождество для тройки i, j, k с участием fst/fst/snd; композиция равна единице.
LaTeX
$$$ \\text{cocycle}_{full}(i,j,k) : t'_{\\mathcal{U}} f g i j k \\;\\gg\\; t'_{\\mathcal{U}} f g j k i \\;\\gg\\; t'_{\\mathcal{U}} f g k i j = \\mathbf{1} $$
Lean4
theorem cocycle (i j k : 𝒰.I₀) : t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j = 𝟙 _ :=
by
apply pullback.hom_ext <;> rw [Category.id_comp]
· apply pullback.hom_ext
· apply pullback.hom_ext
· simp_rw [Category.assoc, cocycle_fst_fst_fst 𝒰 f g i j k]
· simp_rw [Category.assoc, cocycle_fst_fst_snd 𝒰 f g i j k]
· simp_rw [Category.assoc, cocycle_fst_snd 𝒰 f g i j k]
· apply pullback.hom_ext
· apply pullback.hom_ext
· simp_rw [Category.assoc, cocycle_snd_fst_fst 𝒰 f g i j k]
· simp_rw [Category.assoc, cocycle_snd_fst_snd 𝒰 f g i j k]
· simp_rw [Category.assoc, cocycle_snd_snd 𝒰 f g i j k]
