English
Assuming IsDomain, PID, CharZero and NoZeroSmulDivisors, there exist integers a,b with b>0 such that for all x in corootSpace α, (a α + b χ) x = 0 for some χ and α with χ ≠ 0 and genWeightSpace χ nontrivial.
Русский
Пусть R удовлетворяет условиям: домен, PID, CharZero и NoZeroSmulDivisors; существуют a,b с b>0 такие, что для любого x ∈ corootSpace α выполняется (a α + b χ) x = 0
LaTeX
$$$\exists a,b \in \mathbb{Z}, 0 < b \wedge \forall x \in \operatorname{corootSpace}(\alpha), (a \cdot α + b \cdot χ) (x) = 0$$$
Lean4
theorem trace_toEnd_genWeightSpaceChain_eq_zero (hp : genWeightSpace M (p • α + χ) = ⊥)
(hq : genWeightSpace M (q • α + χ) = ⊥) {x : H} (hx : x ∈ corootSpace α) :
LinearMap.trace R _ (toEnd R H (genWeightSpaceChain M α χ p q) x) = 0 :=
by
rw [LieAlgebra.mem_corootSpace'] at hx
induction hx using Submodule.span_induction with
| mem u hu =>
obtain ⟨y, hy, z, hz, hyz⟩ := hu
let f : Module.End R (genWeightSpaceChain M α χ p q) :=
{ toFun := fun ⟨m, hm⟩ ↦
⟨⁅(y : L), m⁆, lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M α χ p q hq hy hm⟩
map_add' := fun _ _ ↦ by simp
map_smul' := fun t m ↦ by simp }
let g : Module.End R (genWeightSpaceChain M α χ p q) :=
{ toFun := fun ⟨m, hm⟩ ↦
⟨⁅(z : L), m⁆, lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left M α χ p q hp hz hm⟩
map_add' := fun _ _ ↦ by simp
map_smul' := fun t m ↦ by simp }
have hfg : toEnd R H _ u = ⁅f, g⁆ := by
ext
rw [toEnd_apply_apply, LieSubmodule.coe_bracket, LieSubalgebra.coe_bracket_of_module, ← hyz]
simp only [lie_lie, LieHom.lie_apply, LinearMap.coe_mk, AddHom.coe_mk, Module.End.lie_apply,
AddSubgroupClass.coe_sub, f, g]
simp [hfg]
| zero => simp
| add => simp_all
| smul => simp_all
