cocyclesMk — Mathlib

English

From an element f of the kernel of the nth differential, one obtains an n-cocycle in Z^n(G,A).

Русский

Из элемента f в ядре n-го дифференциала получается n-коциклы в Z^n(G,A).

LaTeX

$$$$ \\text{cocyclesMk}(f,h) \\in Z^n(G,A) \\quad \\text{when } h: d^n f = 0. $$$$

Lean4

/-- Make an `n`-cocycle out of an element of the kernel of the `n`th differential. -/
abbrev cocyclesMk {n : ℕ} (f : (Fin n → G) → A) (h : inhomogeneousCochains.d A n f = 0) : cocycles A n :=
  (inhomogeneousCochains A).cyclesMk f (n + 1) (by simp) (by simp [h])

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