mem_cocycles₁_def — Mathlib

English

An element f in G → A lies in Z^1(G,A) iff it satisfies the cocycle equation ∀ g,h: ρ(g)(f(h)) − f(gh) + f(g) = 0.

Русский

Элемент f: G → A принадлежит Z^1(G,A), если выполняется равенство кокицела: ∀ g,h: ρ(g)(f(h)) − f(gh) + f(g) = 0.

LaTeX

$$$f ∈ cocycles_1 A \\iff ∀ g h : G, A.ρ g (f h) - f (g h) + f g = 0$$$

Lean4

theorem mem_cocycles₁_def (f : G → A) : f ∈ cocycles₁ A ↔ ∀ g h : G, A.ρ g (f h) - f (g * h) + f g = 0 :=
  LinearMap.mem_ker.trans <| by
    simp_rw [funext_iff, d₁₂_hom_apply, Prod.forall]
    rfl

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