restrict_killingForm_eq_sum — Mathlib

English

The Killing form restricted to H decomposes as a sum of rank-one bilinear forms coming from the roots: κ|_H = sum_{α in H.root} α ⊗ α.

Русский

Киллинг-форма, ограниченная на H, раскладывается в сумму рангово-однозначных билинейных форм, полученных из корней: κ|_H = ∑_{α ∈ H.root} α ⊗ α.

LaTeX

$$$(\\kappa_{K,L})|_H = \\displaystyle\\sum_{\\alpha \\in H.root} \\alpha \\otimes \\alpha,$$$

Lean4

theorem restrict_killingForm_eq_sum :
    (killingForm K L).restrict H = ∑ α ∈ H.root, (α : H →ₗ[K] K).smulRight (α : H →ₗ[K] K) :=
  by
  rw [restrict_killingForm, traceForm_eq_sum_finrank_nsmul' K H L]
  refine Finset.sum_congr rfl fun χ hχ ↦ ?_
  replace hχ : χ.IsNonZero := by simpa [LieSubalgebra.root] using hχ
  simp [finrank_rootSpace_eq_one _ hχ]

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