English
If x ∈ L and χ ∈ R, the maxGenEigenspace of the endomorphism toEnd_R(L)(x) with eigenvalue χ is the largest subspace on which x acts with eigenvalue χ. The lemma identifies this subspace with a corresponding weight component of a module.
Русский
Если x ∈ L и χ ∈ R, то maxGenEigenspace для эндоморфизма toEnd_R(L)(x) с собственным значением χ является наибольшим по размеру подпространством, на котором x действует с собственным значением χ; лемма связывает это с весовым компонентом модуля.
LaTeX
$$$\\maxGenEigenspace_{χ}^{x} = \\{ m \\mid (\\,.toEnd_R(L,M)x-χ\\cdot \\mathrm{id}\\,)^{k} m = 0 \\text{ forSome } k \\}$$$
Lean4
theorem lie_mem_maxGenEigenspace_toEnd {χ₁ χ₂ : R} {x y : L} {m : M} (hy : y ∈ 𝕎(L, χ₁, x)) (hm : m ∈ 𝕎(M, χ₂, x)) :
⁅y, m⁆ ∈ 𝕎(M, χ₁ + χ₂, x) :=
by
apply LieModule.weight_vector_multiplication L M M (toModuleHom R L M) χ₁ χ₂
simp only [LieModuleHom.coe_toLinearMap, Function.comp_apply, LinearMap.coe_comp, TensorProduct.mapIncl,
LinearMap.mem_range]
use ⟨y, hy⟩ ⊗ₜ ⟨m, hm⟩
simp only [Submodule.subtype_apply, toModuleHom_apply, TensorProduct.map_tmul]
