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., [serre1965](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]
:
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.
- A : Matrix ι ι ℤ
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.
- cartan : LieSubalgebra R L
The span of the
h, included to give definitional control. - cartan_eq_lieSpan : self.cartan = LieSubalgebra.lieSpan R L (Set.range self.h)
- 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]
(b : Basis ι R L)
[IsAddTorsionFree L]
(i : ι)
:
b.A i i = 2
@[simp]
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]
(b : Basis ι R L)
:
b.cartan.toSubmodule = Submodule.span R (Set.range b.h)
instance
LieAlgebra.Basis.instIsLieAbelianSubtypeMemLieSubalgebraCartan
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(b : Basis ι R L)
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
def
LieAlgebra.Basis.h'
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(b : Basis ι R L)
(i : ι)
:
↥b.cartan
As shown in LieAlgebra.Basis.coroot_eq_h' this is a coroot.
Instances For
@[simp]
def
LieAlgebra.Basis.borelUpper
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(b : Basis ι R L)
:
LieSubmodule R (↥b.cartan) L
The nilpotent part of the "upper" Borel subalgebra assocated to a basis.
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]
(b : Basis ι R L)
:
LieSubmodule R (↥b.cartan) L
The nilpotent part of the "lower" Borel subalgebra assocated to a basis.
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]
(b : Basis ι R L)
:
iSup ![b.cartan.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤
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]
(b : Basis ι R L)
[Fintype ι]
(i : ι)
:
Module.Dual R ↥b.cartan
These elements constitute a base for the root system of the Lie algebra relative to the associated Cartan subalgebra.
Instances For
@[simp]
theorem
LieAlgebra.Basis.iSupIndep_rootSpace
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(b : Basis ι R L)
[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]
(b : Basis ι R L)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
:
b.cartan.toLieSubmodule = rootSpace b.cartan 0
theorem
LieAlgebra.Basis.borelLower_eq
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(b : Basis ι R L)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
:
b.borelLower = ⨆ (n : ι → ℕ), ⨆ (_ : n ≠ 0), rootSpace b.cartan (∑ i : ι, n i • ⇑((-b.baseSupp) i))
theorem
LieAlgebra.Basis.borelUpper_eq
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(b : Basis ι R L)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
:
b.borelUpper = ⨆ (n : ι → ℕ), ⨆ (_ : n ≠ 0), rootSpace b.cartan (∑ i : ι, n i • ⇑(b.baseSupp i))
instance
LieAlgebra.Basis.instIsCartanSubalgebraCartanOfIsNoetherian
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(b : Basis ι R L)
[Fintype ι]
[IsDomain R]
[CharZero R]
[Module.IsTorsionFree R L]
[IsNoetherian R L]
:
noncomputable def
LieAlgebra.Basis.baseSupp'
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
(i : ι)
:
The elements LieAlgebra.Basis.baseSupp as roots in the sense of LieSubalgebra.root.
Instances For
@[simp]
theorem
LieAlgebra.Basis.coe_linearMap_baseSupp'
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
(i : ι)
:
LieModule.Weight.toLinear K (↥b.cartan) L ↑(b.baseSupp' i) = b.baseSupp i
theorem
LieAlgebra.Basis.linearIndepOn_root_baseSupp
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
[LieModule.IsTriangularizable K (↥b.cartan) L]
[IsKilling K L]
:
LinearIndepOn K (⇑(IsKilling.rootSystem b.cartan).root) (Set.range b.baseSupp')
theorem
LieAlgebra.Basis.root_mem_or_mem_neg
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
[LieModule.IsTriangularizable K (↥b.cartan) L]
[IsKilling K L]
(χ : ↥LieSubalgebra.root)
:
(IsKilling.rootSystem b.cartan).root χ ∈ AddSubmonoid.closure (⇑(IsKilling.rootSystem b.cartan).root '' Set.range b.baseSupp') ∨ -(IsKilling.rootSystem b.cartan).root χ ∈ AddSubmonoid.closure (⇑(IsKilling.rootSystem b.cartan).root '' Set.range b.baseSupp')
noncomputable def
LieAlgebra.Basis.base
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
[LieModule.IsTriangularizable K (↥b.cartan) L]
[IsKilling K L]
:
The distinguished root system base associated to a basis.
Instances For
noncomputable def
LieAlgebra.Basis.baseSupportEquiv
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
[LieModule.IsTriangularizable K (↥b.cartan) L]
[IsKilling K L]
:
The support of LieAlgebra.Basis.base is in one-to-one correspondence with the indexing
set of the basis.
Instances For
@[simp]
theorem
LieAlgebra.Basis.coe_baseSupportEquiv_apply
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
[LieModule.IsTriangularizable K (↥b.cartan) L]
[IsKilling K L]
(i : ι)
:
LieModule.Weight.toLinear K (↥b.cartan) L ↑↑(b.baseSupportEquiv i) = b.baseSupp i
@[simp]
theorem
LieAlgebra.Basis.coroot_eq_h'
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
[LieModule.IsTriangularizable K (↥b.cartan) L]
[IsKilling K L]
(i : ι)
:
IsKilling.coroot ↑↑(b.baseSupportEquiv i) = b.h' i
theorem
LieAlgebra.Basis.cartanMatrix_base_eq
{ι : Type u_1}
{K : Type u_2}
{L : Type u_3}
[Fintype ι]
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[FiniteDimensional K L]
(b : Basis ι K L)
[LieModule.IsTriangularizable K (↥b.cartan) L]
[IsKilling K L]
:
b.base.cartanMatrix = (Matrix.reindex b.baseSupportEquiv b.baseSupportEquiv) b.A