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]
:
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.
- cartan : LieSubalgebra R L
The span of the
h, included to give definitional control. - 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 : ι)
:
@[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)
:
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)
:
def
LieAlgebra.Basis.symm
{ι : Type u_1}
{R : Type u_2}
{L : Type u_3}
[Finite ι]
[CommRing R]
[LieRing L]
[LieAlgebra R L]
(b : Basis ι R L)
:
Basis ι R L
A basis has a natural involution obtained by interchanging the roles of e and f and
negating h.
Equations
- One or more equations did not get rendered due to their size.
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]
(b : Basis ι R L)
:
LieSubmodule R (↥b.cartan) L
The nilpotent part of the "upper" Borel subalgebra assocated 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]
(b : Basis ι R L)
:
LieSubmodule R (↥b.cartan) L
The nilpotent part of the "lower" Borel subalgebra assocated 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]
(b : Basis ι R L)
:
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.
Equations
- b.baseSupp i = ∑ j : ι, b.A i j • ((Module.Basis.span ⋯).map (LinearEquiv.ofEq b.cartan.toSubmodule (Submodule.span R (Set.range b.h)) ⋯).symm).coord j
Instances For
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]
:
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]
:
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]
:
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 : ι)
:
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.
Equations
- b.base = RootPairing.Base.mk' (LieAlgebra.IsKilling.rootSystem b.cartan) (Set.range b.baseSupp') ⋯ ⋯
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.
Equations
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 : ι)
:
@[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 : ι)
:
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]
: