cocycle_snd_fst_snd — Mathlib

English

General cocycle relation tying together t', fst, snd in the gluing construction for pullbacks.

Русский

Общее кокосовое отношение, связывающее t', fst и snd в конструкции склейки для обратных диаграмм.

LaTeX

$$$ \\text{cocycle}_{general}(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_snd_fst_snd (i j k : 𝒰.I₀) :
    t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _ :=
  by simp only [pullback.condition_assoc, t'_snd_fst_snd]

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