Relations in Geck's construction of a Lie algebra associated to a root system

This file contains proofs that RootPairing.GeckConstruction.lieAlgebra contains sl₂ triples satisfying relations associated to the Cartan matrix of the input root system.

Main definitions:

• RootPairing.GeckConstruction.isSl2Triple: a distinguished family of sl₂ triples contained in the Geck construction.
• RootPairing.GeckConstruction.lie_h_e: an interaction relation between different sl₂ triples.
• RootPairing.GeckConstruction.lie_h_f: an interaction relation between different sl₂ triples.
• RootPairing.GeckConstruction.lie_e_f_ne: an interaction relation between different sl₂ triples.

theorem RootPairing.GeckConstruction.lie_h_e {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [Fintype ι] (i j : { x : ι // x ∈ b.support }) : ⁅h j, e i⁆ = b.cartanMatrix i j • e i

Lemma 3.3 (a) from Geck.

theorem RootPairing.GeckConstruction.lie_h_f {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [Fintype ι] (i j : { x : ι // x ∈ b.support }) : ⁅h j, f i⁆ = -b.cartanMatrix i j • f i

Lemma 3.3 (b) from Geck.

theorem RootPairing.GeckConstruction.lie_e_f_same {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [Fintype ι] (i : { x : ι // x ∈ b.support }) [P.IsReduced] : ⁅e i, f i⁆ = h i

Lemma 3.4 from Geck.

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

theorem RootPairing.GeckConstruction.lie_e_f_ne {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [Fintype ι] {i j : { x : ι // x ∈ b.support }} (hij : i ≠ j) [P.IsReduced] [P.IsIrreducible] : ⁅e i, f j⁆ = 0

Lemma 3.5 from Geck.