English
The orthogonal complement of inner derivations forms a Lie submodule of all derivations; in particular, it contains those derivations that annihilate the inner derivations via the Killing form orthogonality.
Русский
Ортогональная дополняющая часть внутренних производных образует подподмодуль Ли всех дериваций; она сохраняется под действием скобки и удовлетворяет условиям ортогональности по форме Killing.
LaTeX
$$rangeAdOrthogonal : LieSubmodule R L (LieDerivation R L L)$$
Lean4
/-- The orthogonal complement of the inner derivations is a Lie submodule of all derivations. -/
@[simps!]
noncomputable def rangeAdOrthogonal : LieSubmodule R L (LieDerivation R L L)
where
__ := 𝕀ᗮ
lie_mem := by
intro x D hD
have : 𝕀ᗮ = (ad R L).idealRange.killingCompl := by simp [← (ad_isIdealMorphism R L).eq]
change D ∈ 𝕀ᗮ at hD
change ⁅x, D⁆ ∈ 𝕀ᗮ
rw [this] at hD ⊢
rw [← lie_ad]
exact lie_mem_right _ _ (ad R L).idealRange.killingCompl _ _ hD
