English
For a weight χ, the trace of the endomorphism given by x on the weight space genWeightSpace M χ equals the dimension of genWeightSpace M χ times χ(x).
Русский
Траcея эндоморфизма, соответствующего элементу x, на весовом пространстве χ равна размерности этого весового пространства, умноженной на χ(x).
LaTeX
$$$\operatorname{tr}\bigl(\mathrm{toEnd}(R,L,\mathrm{genWeightSpace}(M,\chi),x)\bigr) = \operatorname{finrank}_R(\mathrm{genWeightSpace}(M,\chi)) \cdot \chi(x)$$$
Lean4
@[simp]
theorem trace_toEnd_genWeightSpace [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M]
(χ : L → R) (x : L) : trace R _ (toEnd R L (genWeightSpace M χ) x) = finrank R (genWeightSpace M χ) • χ x :=
by
suffices _root_.IsNilpotent ((toEnd R L (genWeightSpace M χ) x) - χ x • LinearMap.id)
by
replace this := (isNilpotent_trace_of_isNilpotent this).eq_zero
rwa [map_sub, map_smul, trace_id, sub_eq_zero, smul_eq_mul, mul_comm, ← nsmul_eq_mul] at this
rw [← Module.algebraMap_end_eq_smul_id]
exact isNilpotent_toEnd_sub_algebraMap M χ x
