boundaries₂ — Mathlib

English

The 2-boundaries B2(G,A) are defined as the image of the map d32: (G³ →₀ A) → (G² →₀ A).

Русский

2‑границы B2(G,A) задаются как образ отображения d32: (G³ →₀ A) → (G² →₀ A).

LaTeX

$$B_2(G,A) = Im(d_{32} : (G^3 →₀ A) → (G^2 →₀ A))$$

Lean4

/-- The 2-boundaries `B₂(G, A)` of `A : Rep k G`, defined as the image of the map
`(G³ →₀ A) → (G² →₀ A)` defined by
`a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂)`. -/
def boundaries₂ : Submodule k (G × G →₀ A) :=
  LinearMap.range (d₃₂ A).hom

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