coboundaries₁ — Mathlib

English

The first coboundaries B¹(G,A) are the image of the map d₀₁ from A to (G → A).

Русский

Первые границы B¹(G,A) являются образом отображения d₀₁: A → (G → A).

LaTeX

$$$$ coboundaries_1(A) = range(d_{0 1} A).hom. $$$$

Lean4

/-- The 1-coboundaries `B¹(G, A)` of `A : Rep k G`, defined as the image of the map
`A → Fun(G, A)` sending `(a, g) ↦ ρ_A(g)(a) - a.` -/
def coboundaries₁ : Submodule k (G → A) :=
  LinearMap.range (d₀₁ A).hom

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