English
For any α,β roots with α+β ≠ 0, the Killing form pairs x ∈ rootSpace α and y ∈ rootSpace β to zero.
Русский
Для любых корневых пространств α и β с α+β ≠ 0, Killing-форма скрещивает x ∈ rootSpace α и y ∈ rootSpace β в ноль.
LaTeX
$$$ \\kappa(x,y) = 0 \\quad\\text{if } x \\in \\mathfrak{g}_α,\\ y \\in \\mathfrak{g}_β,\\ α+β \\neq 0 $$$
Lean4
/-- For any `α` and `β`, the corresponding root spaces are orthogonal with respect to the Killing
form, provided `α + β ≠ 0`. -/
theorem killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero {α β : H → K} {x y : L} (hx : x ∈ rootSpace H α)
(hy : y ∈ rootSpace H β) (hαβ : α + β ≠ 0) : killingForm K L x y = 0 := by
/- If `ad R L z` is semisimple for all `z ∈ H` then writing `⟪x, y⟫ = killingForm K L x y`, there
is a slick proof of this lemma that requires only invariance of the Killing form as follows.
For any `z ∈ H`, we have:
`α z • ⟪x, y⟫ = ⟪α z • x, y⟫ = ⟪⁅z, x⁆, y⟫ = - ⟪x, ⁅z, y⁆⟫ = - ⟪x, β z • y⟫ = - β z • ⟪x, y⟫`.
Since this is true for any `z`, we thus have: `(α + β) • ⟪x, y⟫ = 0`, and hence the result.
However the semisimplicity of `ad R L z` is (a) non-trivial and (b) requires the assumption
that `K` is a perfect field and `L` has non-degenerate Killing form. -/
let σ : (H → K) → (H → K) := fun γ ↦ α + (β + γ)
have hσ : ∀ γ, σ γ ≠ γ := fun γ ↦ by simpa only [σ, ← add_assoc] using add_ne_right.mpr hαβ
let f : Module.End K L := (ad K L x) ∘ₗ (ad K L y)
have hf : ∀ γ, MapsTo f (rootSpace H γ) (rootSpace H (σ γ)) := fun γ ↦
(mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α (β + γ) hx).comp <|
mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L β γ hy
classical
have hds :=
DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
(LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpace K H L)
(LieSubmodule.iSup_toSubmodule_eq_top.mpr <| iSup_genWeightSpace_eq_top K H L)
exact LinearMap.trace_eq_zero_of_mapsTo_ne hds σ hσ hf
