iCocycles_mk — Mathlib

English

If f is any n-cochain, and h expresses that d^n f = 0, then iCocycles A n (cocyclesMk f h) = f.

Русский

Если f — произвольная n-коцепа и h выражает, что d^n f = 0, тогда iCocycles A n (cocyclesMk f h) = f.

LaTeX

$$$$ iCocycles A n (cocyclesMk f h) = f. $$$$

Lean4

theorem iCocycles_mk {n : ℕ} (f : (Fin n → G) → A) (h : inhomogeneousCochains.d A n f = 0) :
    iCocycles A n (cocyclesMk f h) = f := by
  exact (inhomogeneousCochains A).i_cyclesMk (i := n) f (n + 1) (by simp) (by simp [h])

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