Geck's construction of a Lie algebra associated to a root system yields semisimple algebras

This file contains a proof that RootPairing.GeckConstruction.lieAlgebra yields semisimple Lie algebras.

Main definitions:

• RootPairing.GeckConstruction.trace_toEnd_eq_zero: the Geck construction yields trace-free matrices.
• RootPairing.GeckConstruction.instIsIrreducible: the defining representation of the Geck construction is irreducible.
• RootPairing.GeckConstruction.instHasTrivialRadical: the Geck construction yields semisimple Lie algebras.

theorem RootPairing.GeckConstruction.isNilpotent_e {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] [P.IsReduced] {b : P.Base} [Fintype ι] [DecidableEq ι] (i : { x : ι // x ∈ b.support }) : IsNilpotent (e i)

theorem RootPairing.GeckConstruction.isNilpotent_f {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] [P.IsReduced] {b : P.Base} [Fintype ι] [DecidableEq ι] (i : { x : ι // x ∈ b.support }) : IsNilpotent (f i)

@[simp]

theorem RootPairing.GeckConstruction.trace_h_eq_zero {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base} [Fintype ι] [DecidableEq ι] (i : { x : ι // x ∈ b.support }) : (h i).trace = 0

theorem RootPairing.GeckConstruction.trace_toEnd_eq_zero {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] [P.IsReduced] {b : P.Base} [Fintype ι] [DecidableEq ι] (x : ↥(lieAlgebra b)) : (LinearMap.trace R ({ x : ι // x ∈ b.support } ⊕ ι → R)) ((LieModule.toEnd R (↥(lieAlgebra b)) ({ x : ι // x ∈ b.support } ⊕ ι → R)) x) = 0

This is the main result of lemma 4.1 from Geck.

theorem RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [CharZero K] [DecidableEq ι] [Fintype ι] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootSystem ι K M N} [P.IsCrystallographic] {b : P.Base} : ↑(LieModule.genWeightSpace ({ x : ι // x ∈ b.support } ⊕ ι → K) 0) = Submodule.span K (Set.range u)

instance RootPairing.GeckConstruction.instIsIrreducible {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [CharZero K] [DecidableEq ι] [Fintype ι] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootSystem ι K M N} [P.IsCrystallographic] {b : P.Base} [Fact ((4 - b.cartanMatrix).det ≠ 0)] [P.IsReduced] [P.IsIrreducible] [Nonempty ι] : LieModule.IsIrreducible K (↥(lieAlgebra b)) ({ x : ι // x ∈ b.support } ⊕ ι → K)

Lemma 4.2 from Geck.

instance RootPairing.GeckConstruction.instHasTrivialRadical {ι : Type u_1} {K : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [CharZero K] [DecidableEq ι] [Fintype ι] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] {P : RootSystem ι K M N} [P.IsCrystallographic] {b : P.Base} [Fact ((4 - b.cartanMatrix).det ≠ 0)] [P.IsReduced] [P.IsIrreducible] [IsAlgClosed K] : LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)

Lemma 4.3 from Geck.