Bases of semisimple Lie algebras #
In this file we define bases of semisimple Lie algebras. Given an indexing type ι, a basis of a
Lie algebra consists of a non-degenerate matrix of integers A indexed by ι × ι and generators
h i, e i, f i indexed by ι, each forming an sl₂ triple, and satisfying the Chevalley-Serre
relations:
This concept appears not to have a name in the informal literature and so we call it simply a basis.
With further axioms (constraining the structure constants which appear in products of the form
⁅e i, e j⁆, ⁅f i, f j⁆) one obtains the concept of a Weyl or Chevalley basis.
See e.g., [Ser87](Ch. V, §4, §6).
Main definitions / results: #
LieAlgebra.Basis: the concept of a basis for a Lie algebra.LieAlgebra.Basis.cartanMatrix_base_eq: the matrix of aLieAlgebra.Basisis the Cartan matrix of the associated based root system.
TODO #
- Show that every semisimple Lie algebra has a basis.
- Define Weyl, Chevalley bases.
structure
LieAlgebra.Basis
(ι : Type u_1)
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(H : LieSubalgebra R L)
:
Type (max u_1 u_3)
A basis for a semisimple Lie algebra distinguishes a natural Cartan subalgebra and a base for the associated root system.
The Cartan matrix.
- h : ι → L
The basis for the Cartan subalgebra.
- e : ι → L
The generators of the upper Borel subalgebra.
- f : ι → L
The generators of the lower Borel subalgebra.
- linInd : LinearIndependent R self.h
- nondegen : self.A.Nondegenerate
- sl2 (i : ι) : IsSl2Triple (self.h i) (self.e i) (self.f i)
Instances For
@[simp]
theorem
LieAlgebra.Basis.A_diag_eq_two
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[IsAddTorsionFree L]
(i : ι)
:
theorem
LieAlgebra.Basis.coe_cartan_eq_span
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
theorem
LieAlgebra.Basis.isLieAbelian_cartan
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
IsLieAbelian ↥H
def
LieAlgebra.Basis.symm
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
Basis ι H
A basis has a natural involution obtained by interchanging the roles of e and f and
negating h.
Equations
Instances For
@[simp]
theorem
LieAlgebra.Basis.symm_e
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
@[simp]
theorem
LieAlgebra.Basis.symm_A
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
@[simp]
theorem
LieAlgebra.Basis.symm_f
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
@[simp]
theorem
LieAlgebra.Basis.symm_symm
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
def
LieAlgebra.Basis.h'
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
(i : ι)
:
↥H
As shown in LieAlgebra.Basis.coroot_eq_h' this is a coroot.
Instances For
def
LieAlgebra.Basis.borelUpper
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
LieSubmodule R (↥H) L
The nilpotent part of the "upper" Borel subalgebra associated to a basis.
Equations
- b.borelUpper = { toSubmodule := (LieSubalgebra.lieSpan R L (Set.range b.e)).toSubmodule, lie_mem := ⋯ }
Instances For
def
LieAlgebra.Basis.borelLower
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
LieSubmodule R (↥H) L
The nilpotent part of the "lower" Borel subalgebra associated to a basis.
Equations
- b.borelLower = { toSubmodule := (LieSubalgebra.lieSpan R L (Set.range b.f)).toSubmodule, lie_mem := ⋯ }
Instances For
theorem
LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
:
Lemma 4.5 from Geck.
noncomputable def
LieAlgebra.Basis.baseSupp
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
(i : ι)
:
Module.Dual R ↥H
These elements constitute a base for the root system of the Lie algebra relative to the associated Cartan subalgebra.
Equations
- b.baseSupp i = ∑ j : ι, b.A i j • ((Module.Basis.span ⋯).map (LinearEquiv.ofEq H.toSubmodule (Submodule.span R (Set.range b.h)) ⋯).symm).coord j
Instances For
theorem
LieAlgebra.Basis.linearIndependent_baseSupp
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
[IsDomain R]
[CharZero R]
:
theorem
LieAlgebra.Basis.borelUpper_le_biSup
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
[IsDomain R]
[CharZero R]
:
Lemma 4.4 from Geck.
theorem
LieAlgebra.Basis.borelLower_le_biSup
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
[IsDomain R]
[CharZero R]
:
Lemma 4.4 from Geck.
theorem
LieAlgebra.Basis.iSupIndep_rootSpace
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
:
theorem
LieAlgebra.Basis.cartan_eq
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
:
theorem
LieAlgebra.Basis.borelLower_eq
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
:
theorem
LieAlgebra.Basis.borelUpper_eq
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
:
theorem
LieAlgebra.Basis.isCartanSubalgebra
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
{H : LieSubalgebra R L}
(b : Basis ι H)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
[IsNoetherian R L]
: