Geck's construction is complete

The Geck construction of a Lie algebra associated to a root system, RootPairing.GeckConstruction.lieAlgebra, yields a simple Lie algebra. In this file we show that this construction yields all finite-dimensional simple Lie algebras up to isomorphism.

Main definitions / results:

• RootPairing.GeckConstruction.basis: the Geck construction yields a basis.
• RootPairing.GeckConstruction.equivRootSystem: up to equivalence, LieAlgebra.IsKilling.rootSystem is left inverse to RootPairing.GeckConstruction.lieAlgebra.
• RootPairing.GeckConstruction.equivLieAlgebra: up to equivalence, LieAlgebra.IsKilling.rootSystem is right inverse to RootPairing.GeckConstruction.lieAlgebra.

noncomputable def RootPairing.GeckConstruction.basis {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [DecidableEq ι] [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) (cartanSubalgebra' b)

The Geck construction yields a basis of the Lie algebra it constructs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RootPairing.GeckConstruction.basis_A_eq {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [DecidableEq ι] [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' {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [DecidableEq ι] [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) : (cartanSubalgebra' b).IsCartanSubalgebra

noncomputable def RootPairing.GeckConstruction.equivRootSystem {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [DecidableEq ι] [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) [IsAlgClosed K] : P.Equiv (LieAlgebra.IsKilling.rootSystem (cartanSubalgebra' b))

Up to equivalence, LieAlgebra.IsKilling.rootSystem is left inverse to RootPairing.GeckConstruction.lieAlgebra.

Equations

• RootPairing.GeckConstruction.equivRootSystem b = b.equivOfCartanMatrixEq (RootPairing.GeckConstruction.basis b).base (RootPairing.GeckConstruction.basis b).baseSupportEquiv ⋯

instance RootPairing.GeckConstruction.instIsSimpleSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebra {K : Type u_1} [Field K] [CharZero K] {ι : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [DecidableEq ι] [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) [IsAlgClosed K] : LieAlgebra.IsSimple K ↥(lieAlgebra b)

noncomputable def RootPairing.GeckConstruction.equivLieAlgebra {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {L : Type u_2} [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsSimple K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : L ≃ₗ⁅K⁆ ↥(lieAlgebra b)

LieAlgebra.IsKilling.rootSystem is right inverse to RootPairing.GeckConstruction.lieAlgebra.

Equations

• RootPairing.GeckConstruction.equivLieAlgebra H b = LieAlgebra.equivOfRootSystemEquiv (RootPairing.GeckConstruction.equivRootSystem b)