Invariant bilinear forms on a simple Lie algebra are multiples of the Killing form

Let L be a finite-dimensional Lie algebra over an algebraically closed field K whose adjoint module is irreducible (for instance a simple Lie algebra) and whose Killing form is nondegenerate (LieAlgebra.IsKilling). The Killing form is then a nonzero invariant form on the irreducible module L, so by TauCeti.LieModule.exists_eq_smul_of_lieInvariant every invariant bilinear form on L is a scalar multiple of it. In particular every invariant form on L is symmetric, and the invariant symmetric forms TauCeti.LieModule.invariantForms K L L are the line spanned by the Killing form.

In characteristic zero a finite-dimensional simple Lie algebra is Killing (Cartan's criterion, LieAlgebra.HasTrivialRadical.instIsKilling), so this covers every finite-dimensional simple Lie algebra over an algebraically closed field of characteristic zero.

Main results

• TauCeti.LieAlgebra.exists_eq_smul_killingForm: every invariant bilinear form on L is a scalar multiple of the Killing form.
• TauCeti.LieAlgebra.isSymm_of_lieInvariant: every invariant bilinear form on L is symmetric.
• TauCeti.LieAlgebra.invariantForms_eq_span_killingForm and TauCeti.LieAlgebra.finrank_invariantForms_eq_one: the invariant symmetric forms on L are the line spanned by the Killing form.
• TauCeti.LieAlgebra.finrank_invariantForms_pi_eq_card: a finite product of such Lie algebras has one independent invariant symmetric form per factor.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §5.1 for the Killing form and §6.1 for Schur's lemma.

theorem TauCeti.LieAlgebra.exists_eq_smul_killingForm {K : Type u_1} {L : Type u_2} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieModule.IsIrreducible K L L] [LieAlgebra.IsKilling K L] {Φ : LinearMap.BilinForm K L} (hΦ : LinearMap.BilinForm.lieInvariant L Φ) : ∃ (c : K), Φ = c • killingForm K L

Every invariant bilinear form on a Lie algebra is a multiple of the Killing form, for a finite-dimensional Lie algebra over an algebraically closed field whose adjoint module is irreducible and whose Killing form is nondegenerate, such as a simple Lie algebra in characteristic zero.

theorem TauCeti.LieAlgebra.isSymm_of_lieInvariant {K : Type u_1} {L : Type u_2} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieModule.IsIrreducible K L L] [LieAlgebra.IsKilling K L] {Φ : LinearMap.BilinForm K L} (hΦ : LinearMap.BilinForm.lieInvariant L Φ) : Φ.IsSymm

Every invariant bilinear form on a finite-dimensional Lie algebra over an algebraically closed field whose adjoint module is irreducible and whose Killing form is nondegenerate is symmetric.

theorem TauCeti.LieAlgebra.invariantForms_eq_span_killingForm (K : Type u_1) (L : Type u_2) [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieModule.IsIrreducible K L L] [LieAlgebra.IsKilling K L] : LieModule.invariantForms K L L = K ∙ killingForm K L

The invariant symmetric bilinear forms on a finite-dimensional Lie algebra over an algebraically closed field whose adjoint module is irreducible and whose Killing form is nondegenerate are the line spanned by the Killing form.

theorem TauCeti.LieAlgebra.finrank_invariantForms_eq_one (K : Type u_1) (L : Type u_2) [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieModule.IsIrreducible K L L] [LieAlgebra.IsKilling K L] : Module.finrank K ↥(LieModule.invariantForms K L L) = 1

The invariant symmetric bilinear forms on a finite-dimensional Lie algebra over an algebraically closed field whose adjoint module is irreducible and whose Killing form is nondegenerate form a one-dimensional space.

theorem TauCeti.LieAlgebra.finrank_invariantForms_pi_eq_card {K : Type u_1} [Field K] [IsAlgClosed K] {ι : Type u_3} [Fintype ι] (𝔤 : ι → Type u_4) [(i : ι) → LieRing (𝔤 i)] [(i : ι) → LieAlgebra K (𝔤 i)] [∀ (i : ι), FiniteDimensional K (𝔤 i)] [∀ (i : ι), LieModule.IsIrreducible K (𝔤 i) (𝔤 i)] [∀ (i : ι), LieAlgebra.IsKilling K (𝔤 i)] : Module.finrank K ↥(LieModule.invariantForms K ((i : ι) → 𝔤 i) ((i : ι) → 𝔤 i)) = Fintype.card ι

A finite product of simple Killing Lie algebras has one independent invariant symmetric form per factor, over an algebraically closed field.