English
If x ∈ rootSpace(H, α) and y ∈ genWeightSpaceChain(M, α, χ, p, q), then [x,y] ∈ genWeightSpaceChain(M, α, χ, p, q).
Русский
Если x ∈ rootSpace(H, α) и y ∈ genWeightSpaceChain(M, α, χ, p, q), то [x,y] ∈ genWeightSpaceChain(M, α, χ, p, q).
LaTeX
$$$x \in \operatorname{rootSpace}(H, α) \land y \in \operatorname{genWeightSpaceChain}(M, α, χ, p, q) \Rightarrow [x,y] \in \operatorname{genWeightSpaceChain}(M, α, χ, p, q)$$$
Lean4
theorem lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right [LieRing.IsNilpotent H]
(hq : genWeightSpace M (q • α + χ) = ⊥) {x : L} (hx : x ∈ rootSpace H α) {y : M}
(hy : y ∈ genWeightSpaceChain M α χ p q) : ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q :=
by
rw [genWeightSpaceChain, iSup_subtype'] at hy
induction hy using LieSubmodule.iSup_induction' with
| mem k z hz =>
obtain ⟨k, hk⟩ := k
suffices genWeightSpace M ((k + 1) • α + χ) ≤ genWeightSpaceChain M α χ p q
by
apply this
simpa only [zsmul_eq_mul, Int.cast_add, Pi.intCast_def, Int.cast_one] using
(rootSpaceWeightSpaceProduct R L H M α (k • α + χ) ((k + 1) • α + χ) (by rw [add_smul]; abel)
(⟨x, hx⟩ ⊗ₜ ⟨z, hz⟩)).property
rw [genWeightSpaceChain]
rcases eq_or_ne (k + 1) q with rfl | hk'; · simp only [hq, bot_le]
replace hk' : k + 1 ∈ Ioo p q := ⟨by linarith [hk.1], lt_of_le_of_ne hk.2 hk'⟩
exact le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'
| zero => simp
| add _ _ _ _ hz₁ hz₂ => rw [lie_add]; exact add_mem hz₁ hz₂
