English
A bracket relation expresses the Killing form as a scaled Killing pairing via an auxiliary e ∈ L with ⟪e, f⟫ ≠ 0.
Русский
Соотношение bracket выражает Killing-форму через скалированное парное место с помощью опорного e ∈ L, где ⟪e,f⟫ ≠ 0.
LaTeX
$$$ [e,f] = killingForm(K,L)(e,f) \\cdot (cartanEquivDual H)^{-1}(α) $$$
Lean4
theorem lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux {α : Weight K H L} {e f : L}
(heα : e ∈ rootSpace H α) (hfα : f ∈ rootSpace H (-α)) (aux : ∀ (h : H), ⁅h, e⁆ = α h • e) :
⁅e, f⁆ = killingForm K L e f • (cartanEquivDual H).symm α :=
by
set α' := (cartanEquivDual H).symm α
rw [← sub_eq_zero, ← Submodule.mem_bot (R := K), ← ker_killingForm_eq_bot]
apply mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg (α := (0 : H → K))
· simp only [rootSpace_zero_eq, LieSubalgebra.mem_toLieSubmodule]
refine sub_mem ?_ (H.smul_mem _ α'.property)
simpa using mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace K L H L α (-α) heα hfα
· intro z hz
replace hz : z ∈ H := by simpa using hz
have he : ⁅z, e⁆ = α ⟨z, hz⟩ • e := aux ⟨z, hz⟩
have hαz : killingForm K L α' (⟨z, hz⟩ : H) = α ⟨z, hz⟩ :=
LinearMap.BilinForm.apply_toDual_symm_apply (hB := traceForm_cartan_nondegenerate K L H) _ _
simp [traceForm_comm K L L ⁅e, f⁆, ← traceForm_apply_lie_apply, he, mul_comm _ (α ⟨z, hz⟩), hαz]
