English
If the Killing form is nondegenerate and H is a Cartan subalgebra, then the kernel of the restricted Killing form on H is trivial.
Русский
Если Killing-форма невыделима и H —Cartan-subalgebra, то ядро ограниченной Killing-формы на H тривиально.
LaTeX
$$$ \\ker\\big((killingForm\\;R\\;L)\\restriction H\\big) = \\{0\\} \\;=\\; \\bot $$$
Lean4
/-- If the Killing form of a Lie algebra is non-singular, it remains non-singular when restricted
to a Cartan subalgebra. -/
theorem ker_restrict_eq_bot_of_isCartanSubalgebra [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L)
[H.IsCartanSubalgebra] : LinearMap.ker ((killingForm R L).restrict H) = ⊥ :=
by
have h : Codisjoint (rootSpace H 0) (LieModule.posFittingComp R H L) :=
(LieModule.isCompl_genWeightSpace_zero_posFittingComp R H L).codisjoint
replace h : Codisjoint (H : Submodule R L) (LieModule.posFittingComp R H L : Submodule R L) := by
rwa [codisjoint_iff, ← LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule, LieSubmodule.top_toSubmodule,
rootSpace_zero_eq R L H, LieSubalgebra.coe_toLieSubmodule, ← codisjoint_iff] at h
suffices this : ∀ m₀ ∈ H, ∀ m₁ ∈ LieModule.posFittingComp R H L, killingForm R L m₀ m₁ = 0 by
simp [LinearMap.BilinForm.ker_restrict_eq_of_codisjoint h this]
intro m₀ h₀ m₁ h₁
exact killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting R L H (le_zeroRootSubalgebra R L H h₀) h₁
