ad_mem_ker_killingForm_ad_range_of_mem_orthogonal

English

If D lies in the Killing orthogonal of the range of the adjoint, then ad(D x) lies in the kernel of the Killing form restricted to the range of ad.

Русский

Если D лежит в Killing-ортогональности диапазона adj, то ad(Dx) лежит в ядре формы Killing, ограниченной диапазоном ad.

LaTeX

$$$ad_{R,L}(D x) \in \ker\big( (killingForm\; R\; 𝕀) \;|\; \mathrm{range}(ad_{R,L}) \big).$$$

Lean4

theorem ad_mem_ker_killingForm_ad_range_of_mem_orthogonal {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :
    ad R L (D x) ∈ (LinearMap.ker (killingForm R 𝕀)).map (LieHom.range (ad R L)).subtype :=
  by
  rw [← killingForm_restrict_range_ad]
  exact
    LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl
      ⟨by simp, ad_mem_orthogonal_of_mem_orthogonal hD x⟩

Похожие утверждения