English
Elements x ∈ rootSpace α which are Killing-orthogonal to all rootSpace(-α) lie in the kernel of Killing form.
Русский
Элементы x ∈ rootSpace α, ортогональные Killing ко всем rootSpace(-α), лежат в ядре Killing-формы.
LaTeX
$$$ x \\in \\ker(\\killingForm\\;R\\;L) \\quad\\text{if } x \\in rootSpace(α)\\text{ and } ∀y ∈ rootSpace(-α), \\killingForm(x,y)=0$$$
Lean4
/-- Elements of the `α` root space which are Killing-orthogonal to the `-α` root space are
Killing-orthogonal to all of `L`. -/
theorem mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg {α : H → K} {x : L} (hx : x ∈ rootSpace H α)
(hx' : ∀ y ∈ rootSpace H (-α), killingForm K L x y = 0) : x ∈ LinearMap.ker (killingForm K L) :=
by
rw [LinearMap.mem_ker]
ext y
have hy : y ∈ ⨆ β, rootSpace H β := by simp [iSup_genWeightSpace_eq_top K H L]
induction hy using LieSubmodule.iSup_induction' with
| mem β y hy =>
by_cases hαβ : α + β = 0
· exact hx' _ (add_eq_zero_iff_neg_eq.mp hαβ ▸ hy)
· exact killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero K L H hx hy hαβ
| zero => simp
| add => simp_all
