English
If L is abelian and M has no zero divisors, then weights are linear and compatible with the weight space structure.
Русский
Если L абелева и у M нет нулевых делителей, то веса линейны и совместимы со структурой весовых пространств.
LaTeX
$$$[L,L]=0,\\; \\text{NoZeroSMulDivisors}(R,M) \\Rightarrow \\text{LinearWeights }R\\,L\\,M.$$$
Lean4
/-- For an Abelian Lie algebra, the weights of any Lie module are linear. -/
instance instLinearWeightsOfIsLieAbelian [IsLieAbelian L] [NoZeroSMulDivisors R M] : LinearWeights R L M :=
have aux : ∀ (χ : L → R), genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y :=
by
have h : ∀ x y, Commute (toEnd R L M x) (toEnd R L M y) := fun x y ↦ by
rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]
intro χ hχ x y
simp_rw [Ne, ← LieSubmodule.toSubmodule_inj, genWeightSpace, genWeightSpaceOf, LieSubmodule.iInf_toSubmodule,
LieSubmodule.bot_toSubmodule] at hχ
exact Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute (toEnd R L M).toLinearMap χ _ hχ h x y
{ map_add := aux
map_smul := fun χ hχ t x ↦
by
simp_rw [Ne, ← LieSubmodule.toSubmodule_inj, genWeightSpace, genWeightSpaceOf, LieSubmodule.iInf_toSubmodule,
LieSubmodule.bot_toSubmodule] at hχ
exact Module.End.map_smul_of_iInf_genEigenspace_ne_bot (toEnd R L M).toLinearMap χ _ hχ t x
map_lie := fun χ hχ t x ↦ by rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_add] }
