mem_cocycles₂_def — Mathlib

English

A function f lies in cocycles₂(A) if and only if it satisfies the 2‑cocycle relation: f(g h, j) + f(g, h) = ρ_g(f(h, j)) + f(g, h j) for all g,h,j.

Русский

Функция f принадлежит cocycles₂(A) тогда и только тогда, когда она удовлетворяет 2‑кокцикл условию: f(gh,j) + f(g,h) = ρ_g(f(h,j)) + f(g,hj).

LaTeX

$$$$ f \\in cocycles_2(A) \\iff \\forall g,h,j \\in G, \\\\ f(gh,j) + f(g,h) = A.\\\\rho(g)(f(h,j)) + f(g,hj). $$$$

Lean4

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

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