English
If h,e,f form an sl2-triple with e and f in the appropriate root spaces, then h equals coroot α.
Русский
Если h,e,f образуют тройку sl₂ с e и f в соответствующих корневых пространствах, то h = coroot α.
LaTeX
$$h = coroot α$$
Lean4
theorem _root_.IsSl2Triple.h_eq_coroot {α : Weight K H L} (hα : α.IsNonZero) {h e f : L} (ht : IsSl2Triple h e f)
(heα : e ∈ rootSpace H α) (hfα : f ∈ rootSpace H (-α)) : h = coroot α :=
by
have hef := lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg heα hfα
lift h to H using by simpa only [← ht.lie_e_f, hef] using H.smul_mem _ (Submodule.coe_mem _)
congr 1
have key : α h = 2 := by
have := lie_eq_smul_of_mem_rootSpace heα h
rw [LieSubalgebra.coe_bracket_of_module, ht.lie_h_e_smul K] at this
exact smul_left_injective K ht.e_ne_zero this.symm
suffices ∃ s : K, s • h = coroot α by
obtain ⟨s, hs⟩ := this
replace this : s = 1 := by simpa [root_apply_coroot hα, key] using congr_arg α hs
rwa [this, one_smul] at hs
set α' := (cartanEquivDual H).symm α with hα'
have h_eq : h = killingForm K L e f • α' :=
by
simp only [hα', Subtype.ext_iff, ← ht.lie_e_f, hef]
rw [Submodule.coe_smul_of_tower]
use (2 • (α α')⁻¹) * (killingForm K L e f)⁻¹
have hef₀ : killingForm K L e f ≠ 0 := by
have := ht.h_ne_zero
contrapose! this
simpa [this] using h_eq
rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot]
