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.
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 })
:
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))
:
This is the main result of lemma 4.1 from Geck.