English
The range (image) of the trace form is contained in the span of the weight-to-linear-functionals.
Русский
Образ формы следа лежит в линейной оболочке значений функций весов.
LaTeX
$$range (traceForm K L M) ≤ span K (range (Weight.toLinear K L M))$$
Lean4
theorem traceForm_eq_sum_finrank_nsmul_mul (x y : L) :
traceForm K L M x y = ∑ χ : Weight K L M, finrank K (genWeightSpace M χ) • (χ x * χ y) :=
by
have hxy : ∀ χ : Weight K L M, MapsTo (toEnd K L M x ∘ₗ toEnd K L M y) (genWeightSpace M χ) (genWeightSpace M χ) :=
fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm
classical
have hds :=
DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
(LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace' K L M)
(LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top' K L M)
simp_rw [traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict hds hxy, ←
traceForm_genWeightSpace_eq K L M _ x y]
rfl
