Documentation

Mathlib.Algebra.Lie.InvariantForm

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 #

References #

We follow the short and excellent paper [Die53].

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) :

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
Instances For
    @[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 | nN, Φ.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) :

    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
    Instances For
      @[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 xN, (Φ 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) :
      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) :
      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) :
      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) :

      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⁆.