Lie algebras with non-degenerate invariant bilinear forms are semisimple

In this file we prove that a finite-dimensional Lie algebra over a field is semisimple if it does not have non-trivial abelian ideals and it admits a non-degenerate reflexive invariant bilinear form. Here a form is invariant if it invariant under the Lie bracket in the sense that ⁅x, Φ⁆ = 0 for all x or equivalently, Φ ⁅x, y⁆ z = Φ x ⁅y, z⁆.

Main results

• LieAlgebra.InvariantForm.orthogonal: given a Lie submodule N of a Lie module M, we define its orthogonal complement with respect to a non-degenerate invariant bilinear form Φ as the Lie ideal of elements x such that Φ n x = 0 for all n ∈ N.
• LieAlgebra.InvariantForm.isSemisimple_of_nondegenerate: the main result of this file; a finite-dimensional Lie algebra over a field is semisimple if it does not have non-trivial abelian ideals and admits a non-degenerate invariant reflexive bilinear form.

References

We follow the short and excellent paper [dieudonne1953].

def LinearMap.BilinForm.lieInvariant {R : Type u_1} (L : Type u_2) {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (Φ : LinearMap.BilinForm R M) : Prop

A bilinear form on a Lie module M of a Lie algebra L is invariant if for all x : L and y z : M the condition Φ ⁅x, y⁆ z = -Φ y ⁅x, z⁆ holds.

Equations

• LinearMap.BilinForm.lieInvariant L Φ = ∀ (x : L) (y z : M), (Φ ⁅x, y⁆) z = -(Φ y) ⁅x, z⁆

theorem LinearMap.BilinForm.lieInvariant_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (Φ : LinearMap.BilinForm R M) [LieAlgebra R L] [LieModule R L M] : LinearMap.BilinForm.lieInvariant L Φ ↔ Φ ∈ LieModule.maxTrivSubmodule R L (LinearMap.BilinForm R M)

@[simp]

theorem LieAlgebra.InvariantForm.orthogonal_carrier {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (Φ : LinearMap.BilinForm R M) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N : LieSubmodule R L M) : ↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N) = {m : M | ∀ n ∈ N, Φ.IsOrtho n m}

def LieAlgebra.InvariantForm.orthogonal {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (Φ : LinearMap.BilinForm R M) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N : LieSubmodule R L M) : LieSubmodule R L M

The orthogonal complement of a Lie submodule N with respect to an invariant bilinear form Φ is the Lie submodule of elements y such that Φ x y = 0 for all x ∈ N.

Equations

• LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N = { toSubmodule := Φ.orthogonal ↑N, lie_mem := ⋯ }

@[simp]

theorem LieAlgebra.InvariantForm.orthogonal_toSubmodule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (Φ : LinearMap.BilinForm R M) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N : LieSubmodule R L M) : ↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N) = Φ.orthogonal ↑N

theorem LieAlgebra.InvariantForm.mem_orthogonal {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (Φ : LinearMap.BilinForm R M) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (N : LieSubmodule R L M) (y : M) : y ∈ LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv N ↔ ∀ x ∈ N, (Φ x) y = 0

theorem LieAlgebra.InvariantForm.orthogonal_disjoint {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (Φ : LinearMap.BilinForm R L) (hΦ_nondeg : Φ.Nondegenerate) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (hL : ∀ (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I) (I : LieIdeal R L) (hI : IsAtom I) : Disjoint I (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)

theorem LieAlgebra.InvariantForm.orthogonal_isCompl_coe_submodule {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (Φ : LinearMap.BilinForm K L) (hΦ_nondeg : Φ.Nondegenerate) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (hΦ_refl : Φ.IsRefl) (hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) (I : LieIdeal K L) (hI : IsAtom I) : IsCompl ↑I ↑(LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)

theorem LieAlgebra.InvariantForm.orthogonal_isCompl {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (Φ : LinearMap.BilinForm K L) (hΦ_nondeg : Φ.Nondegenerate) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (hΦ_refl : Φ.IsRefl) (hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) (I : LieIdeal K L) (hI : IsAtom I) : IsCompl I (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)

theorem LieAlgebra.InvariantForm.restrict_nondegenerate {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (Φ : LinearMap.BilinForm K L) (hΦ_nondeg : Φ.Nondegenerate) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (hΦ_refl : Φ.IsRefl) (hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) (I : LieIdeal K L) (hI : IsAtom I) : (Φ.restrict (lieIdealSubalgebra K L I).toSubmodule).Nondegenerate

theorem LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (Φ : LinearMap.BilinForm K L) (hΦ_nondeg : Φ.Nondegenerate) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (hΦ_refl : Φ.IsRefl) (hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) (I : LieIdeal K L) (hI : IsAtom I) : (Φ.restrict (lieIdealSubalgebra K L (LieAlgebra.InvariantForm.orthogonal Φ hΦ_inv I)).toSubmodule).Nondegenerate

@[irreducible]

theorem LieAlgebra.InvariantForm.atomistic {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (Φ : LinearMap.BilinForm K L) (hΦ_nondeg : Φ.Nondegenerate) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (hΦ_refl : Φ.IsRefl) (hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) (I : LieIdeal K L) : sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} = I

theorem LieAlgebra.InvariantForm.isSemisimple_of_nondegenerate {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (Φ : LinearMap.BilinForm K L) (hΦ_nondeg : Φ.Nondegenerate) (hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ) (hΦ_refl : Φ.IsRefl) (hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) : LieAlgebra.IsSemisimple K L

A finite-dimensional Lie algebra over a field is semisimple if it does not have non-trivial abelian ideals and it admits a non-degenerate reflexive invariant bilinear form. Here a form is invariant if it is compatible with the Lie bracket: Φ ⁅x, y⁆ z = Φ x ⁅y, z⁆.