English
If M1, M2, M3 are Lie L-modules and g: M1 ⊗ M2 → M3 is a Lie-module morphism, then for χ1, χ2 ∈ R and x ∈ L, the range of g after the weight-filtered inclusion lies in the weight χ1+χ2 space of M3, i.e., range(g ∘ mapIncl(...)) ⊆ 𝕎(M3, χ1+χ2, x).
Lean4
/-- See also `bourbaki1975b` Chapter VII §1.1, Proposition 2 (ii). -/
protected theorem weight_vector_multiplication (M₁ M₂ M₃ : Type*) [AddCommGroup M₁] [Module R M₁] [LieRingModule L M₁]
[LieModule R L M₁] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] [AddCommGroup M₃]
[Module R M₃] [LieRingModule L M₃] [LieModule R L M₃] (g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃) (χ₁ χ₂ : R) (x : L) :
LinearMap.range ((g : M₁ ⊗[R] M₂ →ₗ[R] M₃).comp (mapIncl 𝕎(M₁, χ₁, x) 𝕎(M₂, χ₂, x))) ≤ 𝕎(M₃, χ₁ + χ₂, x) := by
-- Unpack the statement of the goal.
intro m₃
simp only [TensorProduct.mapIncl, LinearMap.mem_range, LinearMap.coe_comp, LieModuleHom.coe_toLinearMap,
Function.comp_apply, exists_imp, Module.End.mem_maxGenEigenspace]
rintro t rfl
let F : Module.End R M₃ :=
toEnd R L M₃ x -
(χ₁ + χ₂) •
↑1
-- The goal is linear in `t` so use induction to reduce to the case that `t` is a pure tensor.
refine t.induction_on ?_ ?_ ?_
· use 0; simp only [LinearMap.map_zero, LieModuleHom.map_zero]
swap
· rintro t₁ t₂ ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩; use max k₁ k₂
simp only [LieModuleHom.map_add, LinearMap.map_add, Module.End.pow_map_zero_of_le (le_max_left k₁ k₂) hk₁,
Module.End.pow_map_zero_of_le (le_max_right k₁ k₂) hk₂, add_zero]
-- Now the main argument: pure tensors.
rintro ⟨m₁, hm₁⟩ ⟨m₂, hm₂⟩
change
∃ k,
(F ^ k) ((g : M₁ ⊗[R] M₂ →ₗ[R] M₃) (m₁ ⊗ₜ m₂)) =
(0 : M₃)
-- Eliminate `g` from the picture.
let f₁ : Module.End R (M₁ ⊗[R] M₂) := (toEnd R L M₁ x - χ₁ • ↑1).rTensor M₂
let f₂ : Module.End R (M₁ ⊗[R] M₂) := (toEnd R L M₂ x - χ₂ • ↑1).lTensor M₁
have h_comm_square : F ∘ₗ ↑g = (g : M₁ ⊗[R] M₂ →ₗ[R] M₃).comp (f₁ + f₂) :=
by
ext m₁ m₂
simp only [f₁, f₂, F, ← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, sub_tmul, tmul_sub, smul_tmul, lie_tmul_right, tmul_smul,
toEnd_apply_apply, LieModuleHom.map_smul, Module.End.one_apply, LieModuleHom.coe_toLinearMap,
LinearMap.smul_apply, Function.comp_apply, LinearMap.coe_comp, LinearMap.rTensor_tmul, LieModuleHom.map_add,
LinearMap.add_apply, LieModuleHom.map_sub, LinearMap.sub_apply, LinearMap.lTensor_tmul,
AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, LinearMap.coe_restrictScalars]
abel
rsuffices ⟨k, hk⟩ : ∃ k : ℕ, ((f₁ + f₂) ^ k) (m₁ ⊗ₜ m₂) = 0
· use k
change (F ^ k) (g.toLinearMap (m₁ ⊗ₜ[R] m₂)) = 0
rw [← LinearMap.comp_apply, Module.End.commute_pow_left_of_commute h_comm_square, LinearMap.comp_apply, hk,
LinearMap.map_zero]
-- Unpack the information we have about `m₁`, `m₂`.
simp only [Module.End.mem_maxGenEigenspace] at hm₁ hm₂
obtain ⟨k₁, hk₁⟩ := hm₁
obtain ⟨k₂, hk₂⟩ := hm₂
have hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ m₂) = 0 := by
simp only [f₁, hk₁, zero_tmul, LinearMap.rTensor_tmul, LinearMap.rTensor_pow]
have hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ m₂) = 0 := by
simp only [f₂, hk₂, tmul_zero, LinearMap.lTensor_tmul, LinearMap.lTensor_pow]
-- It's now just an application of the binomial theorem.
use k₁ + k₂ - 1
have hf_comm : Commute f₁ f₂ := by
ext m₁ m₂
simp only [f₁, f₂, Module.End.mul_apply, LinearMap.rTensor_tmul, LinearMap.lTensor_tmul,
AlgebraTensorModule.curry_apply, LinearMap.lTensor_tmul, TensorProduct.curry_apply, LinearMap.coe_restrictScalars]
rw [hf_comm.add_pow']
simp only [Finset.sum_apply, LinearMap.coeFn_sum, LinearMap.smul_apply]
-- The required sum is zero because each individual term is zero.
apply Finset.sum_eq_zero
rintro ⟨i, j⟩ hij
suffices (f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ m₂) = 0 by rw [this]; apply smul_zero
rcases Nat.le_or_le_of_add_eq_add_pred (Finset.mem_antidiagonal.mp hij) with hi | hj
· rw [(hf_comm.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hf₁, LinearMap.map_zero]
· rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hf₂, LinearMap.map_zero]
