English
A variant of the previous formula where the sum runs only over nonzero weights.
Русский
Вариант формулы, в котором сумма берётся только по ненулевым весам.
LaTeX
$$traceForm K L M = ∑ χ ∈ {χ : Weight K L M | χ.IsNonZero}, finrank K (genWeightSpace M χ) • (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K)$$
Lean4
/-- A variant of `LieModule.traceForm_eq_sum_finrank_nsmul` in which the sum is taken only over the
non-zero weights. -/
theorem traceForm_eq_sum_finrank_nsmul' :
traceForm K L M =
∑ χ ∈ {χ : Weight K L M | χ.IsNonZero},
finrank K (genWeightSpace M χ) • (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K) :=
by
classical
suffices
∑ χ ∈ {χ : Weight K L M | χ.IsZero}, finrank K (genWeightSpace M χ) • (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K) = 0
by
rw [traceForm_eq_sum_finrank_nsmul, ←
Finset.sum_filter_add_sum_filter_not (p := fun χ : Weight K L M ↦ χ.IsNonZero)]
simp [this]
refine Finset.sum_eq_zero fun χ hχ ↦ ?_
replace hχ : (χ : L →ₗ[K] K) = 0 := by simpa [← Weight.coe_toLinear_eq_zero_iff] using hχ
simp [hχ]
-- The reverse inclusion should also hold: TODO prove this!
