The basis obtained from Geck's construction of Lie algebras from root systems #
The Geck construction of a Lie algebra associated to a root system,
RootPairing.GeckConstruction.lieAlgebra, yields a simple Lie algebra with distinguished basis
which we construct here.
Main definitions / results: #
RootPairing.GeckConstruction.basis: the Geck construction yields a basis.RootPairing.GeckConstruction.equivRootSystem: up to equivalence,LieAlgebra.IsKilling.rootSystemis left inverse toRootPairing.GeckConstruction.lieAlgebra.
noncomputable def
RootPairing.GeckConstruction.basis
{ι : Type u_1}
{K : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[DecidableEq ι]
[Field K]
[CharZero K]
[AddCommGroup M]
[Module K M]
[AddCommGroup N]
[Module K N]
{P : RootPairing ι K M N}
[P.IsReduced]
[P.IsCrystallographic]
[P.IsIrreducible]
[P.IsRootSystem]
(b : P.Base)
:
LieAlgebra.Basis (↥b.support) K ↥(lieAlgebra b)
The Geck construction yields a basis of the Lie algebra it constructs.
Instances For
@[simp]
theorem
RootPairing.GeckConstruction.basis_A_eq
{ι : Type u_1}
{K : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[DecidableEq ι]
[Field K]
[CharZero K]
[AddCommGroup M]
[Module K M]
[AddCommGroup N]
[Module K N]
{P : RootPairing ι K M N}
[P.IsReduced]
[P.IsCrystallographic]
[P.IsIrreducible]
[P.IsRootSystem]
(b : P.Base)
:
(basis b).A = b.cartanMatrix
instance
RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'
{ι : Type u_1}
{K : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[DecidableEq ι]
[Field K]
[CharZero K]
[AddCommGroup M]
[Module K M]
[AddCommGroup N]
[Module K N]
{P : RootPairing ι K M N}
[P.IsReduced]
[P.IsCrystallographic]
[P.IsIrreducible]
[P.IsRootSystem]
(b : P.Base)
:
noncomputable def
RootPairing.GeckConstruction.equivRootSystem
{ι : Type u_1}
{K : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Fintype ι]
[DecidableEq ι]
[Field K]
[CharZero K]
[AddCommGroup M]
[Module K M]
[AddCommGroup N]
[Module K N]
{P : RootPairing ι K M N}
[P.IsReduced]
[P.IsCrystallographic]
[P.IsIrreducible]
[P.IsRootSystem]
(b : P.Base)
[LieAlgebra.IsKilling K ↥(lieAlgebra b)]
[IsAlgClosed K]
:
Up to equivalence, LieAlgebra.IsKilling.rootSystem is left inverse to
RootPairing.GeckConstruction.lieAlgebra.