English
Characterizes membership in the root-associated sl2-subalgebra via root data.
Русский
Характеризует принадлежность корневому sl2-подалгебре через данные корня.
LaTeX
$$x ∈ sl2SubalgebraOfRoot α ⇔ ∃ c1,c2,c3 ∈ K, x = c1 e + c2 f + c3 [e,f]$$
Lean4
/-- The `sl₂` subalgebra associated to a root, regarded as a Lie submodule over the Cartan
subalgebra. -/
noncomputable def sl2SubmoduleOfRoot {α : Weight K H L} (hα : α.IsNonZero) : LieSubmodule K H L
where
__ := sl2SubalgebraOfRoot hα
lie_mem {h} x
hx := by
suffices ⁅(h : L), x⁆ ∈ sl2SubalgebraOfRoot hα by simpa
obtain ⟨h', e, f, ht, heα, hfα⟩ := exists_isSl2Triple_of_weight_isNonZero hα
replace hx : x ∈ sl2SubalgebraOfRoot hα := hx
obtain ⟨c₁, c₂, c₃, rfl⟩ := (mem_sl2SubalgebraOfRoot_iff hα ht heα hfα).mp hx
rw [mem_sl2SubalgebraOfRoot_iff hα ht heα hfα, lie_add, lie_add, lie_smul, lie_smul, lie_smul]
have he_wt : ⁅(h : L), e⁆ = α h • e := lie_eq_smul_of_mem_rootSpace heα h
have hf_wt : ⁅(h : L), f⁆ = (-α) h • f := lie_eq_smul_of_mem_rootSpace hfα h
have hef_zero : ⁅(h : L), ⁅e, f⁆⁆ = 0 :=
by
suffices h_coroot_in_zero : ⁅e, f⁆ ∈ rootSpace H (0 : H → K) from
lie_eq_smul_of_mem_rootSpace h_coroot_in_zero h ▸ (zero_smul K ⁅e, f⁆)
rw [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, rootSpace_zero_eq K L H]
exact (coroot α).property
exact ⟨c₁ * α h, c₂ * (-α h), 0, by simp [he_wt, hf_wt, hef_zero, smul_smul]⟩
