trace_comp_toEnd_genWeightSpace_eq

English

The trace of the endomorphism given by the action on a weight space equals the dimension of that weight space times the weight χ.

Русский

След эндоморфизма действия на весовом пространстве равен размерности этого пространства, умноженной на вес χ.

LaTeX

$$$\\operatorname{tr}\\big(\\mathrm{toEnd}(L,\\mathrm{genWeightSpace}(M,χ))\\big) = \\dim_R(\\mathrm{genWeightSpace}(M,χ)) \\cdot χ.$$$

Lean4

theorem trace_comp_toEnd_genWeightSpace_eq (χ : L → R) :
    LinearMap.trace R _ ∘ₗ (toEnd R L (genWeightSpace M χ)).toLinearMap = finrank R (genWeightSpace M χ) • χ :=
  by
  ext x
  simp

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