charAlgHom — Mathlib

English

For w ∈ AddMonoidAlgebra ℂ W and v ∈ V, the value of charAlgHom he hL w at v equals the sum over the support of w of w a times e(L(v,a)).

Русский

Для w ∈ AddMonoidAlgebra ℂ W и v ∈ V: (charAlgHom he hL w) v = ∑_{a ∈ support(w)} w(a) e(L(v,a)).

LaTeX

$$$\\text{charAlgHom}(he,hL)(w)(v) = \\sum_{a \\in w.support} w(a) \\cdot (e(L(v,a)) ).$$$

Lean4

/-- Algebra homomorphism mapping `w` to `fun v ↦ e (L v w)`. -/
noncomputable def charAlgHom (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2) :
    AddMonoidAlgebra ℂ W →ₐ[ℂ] (V →ᵇ ℂ) :=
  AddMonoidAlgebra.lift ℂ W (V →ᵇ ℂ) (charMonoidHom he hL)

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