English
Under suitable Noetherian and triangularizability assumptions, the trace form equals a finite sum of trace forms on generalized weight spaces. More precisely, for a fixed z ∈ L, the trace form on M decomposes as a sum over finitely many weights χ of the trace form on the corresponding generalized weight spaces generated with respect to z.
Русский
При подходящих условиях беззеркальной теории (Noetherian) и треугольной совместимости представления форму следа разлагается на конечную сумму форм следа на обобщённых весовых пространствах, получаемых для фиксированного z ∈ L; т.е. форма следа по M разлагается на сумму по весам χ над соответствующими весовыми пространствами, образованными относительно z.
LaTeX
$$$traceForm R L M = \sum\chi \in (finite\_genWeightSpaceOf\_ne\_bot R L M z).toFinset,\ traceForm R L (genWeightSpaceOf M \chi z)$$$
Lean4
theorem traceForm_eq_sum_genWeightSpaceOf [NoZeroSMulDivisors R M] [IsNoetherian R M] [IsTriangularizable R L M]
(z : L) :
traceForm R L M = ∑ χ ∈ (finite_genWeightSpaceOf_ne_bot R L M z).toFinset, traceForm R L (genWeightSpaceOf M χ z) :=
by
ext x y
have hxy : ∀ χ : R, MapsTo ((toEnd R L M x).comp (toEnd R L M y)) (genWeightSpaceOf M χ z) (genWeightSpaceOf M χ z) :=
fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm
have hfin : {χ : R | (genWeightSpaceOf M χ z : Submodule R M) ≠ ⊥}.Finite :=
by
convert finite_genWeightSpaceOf_ne_bot R L M z
exact LieSubmodule.toSubmodule_eq_bot (genWeightSpaceOf M _ _)
classical
have h := LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpaceOf R L M z
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top h <| by simp [← LieSubmodule.iSup_toSubmodule]
simp only [LinearMap.coeFn_sum, Finset.sum_apply, traceForm_apply_apply,
LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
exact
Finset.sum_congr (by simp)
(fun χ _ ↦ rfl)
-- In characteristic zero (or even just `LinearWeights R L M`) a stronger result holds (no
-- `⊓ LieAlgebra.center R L`) TODO prove this using `LieModule.traceForm_eq_sum_finrank_nsmul_mul`.
