cocycles₁ — Mathlib

English

The 1-cocycles Z^1(G,A) are defined as the kernel of the differential d12: Fun(G, A) → Fun(G × G, A).

Русский

1-цикл Z^1(G,A) определяется как ядро дифференциала d12: Fun(G, A) → Fun(G × G, A).

LaTeX

$$Z^1(G,A) = Ker(d_{12} A)$$

Lean4

/-- The 1-cocycles `Z¹(G, A)` of `A : Rep k G`, defined as the kernel of the map
`Fun(G, A) → Fun(G × G, A)` sending `(f, (g₁, g₂)) ↦ ρ_A(g₁)(f(g₂)) - f(g₁g₂) + f(g₁).` -/
def cocycles₁ : Submodule k (G → A) :=
  LinearMap.ker (d₁₂ A).hom

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