killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting

English

For an ideal I in L, the submodule I.killingCompl equals the orthogonal of I.toSubmodule with respect to the Killing form.

Русский

Для идеала I в L подмодуль I.killingCompl совпадает с ортогональным дополнением к I.toSubmodule относительно формы Killing.

LaTeX

$$LieSubmodule.toSubmodule I.killingCompl = (killingForm R L).orthogonal I.toSubmodule$$

Lean4

theorem killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting (H : LieSubalgebra R L) [LieRing.IsNilpotent H] {x₀ x₁ : L}
    (hx₀ : x₀ ∈ LieAlgebra.zeroRootSubalgebra R L H) (hx₁ : x₁ ∈ LieModule.posFittingComp R H L) :
    killingForm R L x₀ x₁ = 0 :=
  LieModule.eq_zero_of_mem_genWeightSpace_mem_posFitting R H L
    (fun x y z ↦ LieModule.traceForm_apply_lie_apply' R L L x y z) hx₀ hx₁

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