English
A variant of the previous trace form assertion focusing on the nonzero weight subset as in the previous theorem.
Русский
Вариант утверждения формы следа с акцентом на множество ненулевых весов, как в предыдущем свойстве.
LaTeX
$$traceForm K L M = ∑ χ ∈ {χ : Weight K L M | χ.IsNonZero}, finrank K (genWeightSpace M χ) • (χ : L →ₗ[K] K).smulRight (χ : L →ₗ[K] K)$$
Lean4
theorem range_traceForm_le_span_weight : LinearMap.range (traceForm K L M) ≤ span K (range (Weight.toLinear K L M)) :=
by
rintro - ⟨x, rfl⟩
rw [LieModule.traceForm_eq_sum_finrank_nsmul, LinearMap.coeFn_sum, Finset.sum_apply]
refine Submodule.sum_mem _ fun χ _ ↦ ?_
simp_rw [LinearMap.smul_apply, LinearMap.coe_smulRight, Weight.toLinear_apply, ← Nat.cast_smul_eq_nsmul K]
exact Submodule.smul_mem _ _ <| Submodule.smul_mem _ _ <| subset_span <| mem_range_self χ
