The Chevalley involution of Geck's Lie algebra

Geck's construction realizes a reduced crystallographic root system as an explicit matrix Lie algebra. Mathlib supplies an involutive conjugation exchanging its simple raising and lowering generators, but that conjugation has the unsigned formulas eᵢ ↦ fᵢ and fᵢ ↦ eᵢ.

This file constructs the signed Chevalley involution. First conjugate by the diagonal matrix which acts on the coordinate indexed by a root α through (-1) ^ height(α). Since every simple root has height one, this grading involution fixes hᵢ and negates both eᵢ and fᵢ. Composing it with Mathlib's opposition involution gives

hᵢ ↦ -hᵢ,    eᵢ ↦ -fᵢ,    fᵢ ↦ -eᵢ.

The resulting automorphism is characterized by these equations and is its own inverse. This is the Chevalley involution on the concrete split semisimple Lie algebra produced from a root datum.

Main definitions and results

• TauCeti.geckChevalleyInvolution: the signed involution of Geck's constructed Lie algebra.
• TauCeti.geckChevalleyInvolution_h, TauCeti.geckChevalleyInvolution_e, and TauCeti.geckChevalleyInvolution_f: its values on the Chevalley generators.
• TauCeti.eq_geckChevalleyInvolution: uniqueness from those generator values.
• TauCeti.geckChevalleyInvolution_symm: the involution is its own inverse.

Roadmap

Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md asks for the split reductive group scheme over ℤ to be built "via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra", and insists on constructions rather than existence theorems. The involution constructed here is characterized on the simple generators and supplies the concrete compatibility needed when one later chooses opposite root vectors. Extending it to a normalized root-vector system and proving the resulting sign symmetry of the structure constants remain future work (Humphreys §25.2, Carter §4.1). TauCeti.serreChevalleyInvolution of TauCeti/Algebra/Lie/Presentation/Serre/Automorphism.lean is that automorphism on the presented Lie algebra; this file supplies it on the concrete side. Geck's construction is the explicit realisation of a root datum by a matrix Lie algebra, proved semisimple with the given root system upstream, so it is a carrier of the kind Layer 9 demands, and TauCeti.serreLift_comp_serreChevalleyInvolution transports the presented involution to any such concrete algebra once the two are identified — an identification that needs the generator formulas TauCeti.geckChevalleyInvolution_h, TauCeti.geckChevalleyInvolution_e and TauCeti.geckChevalleyInvolution_f proved here. The Kostant ℤ-form of TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/ is the other named ingredient, and milestone L0 of TauCetiRoadmap/CFSGStatement/README.md is the downstream consumer of the assembled pinned group scheme.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25.2.
• R. W. Carter, Simple Groups of Lie Type, §4.1.

@[instance_reducible]

noncomputable def TauCeti.geckIndexDecidableEq {ι : Type u} : DecidableEq ι

Classical decidable equality on the index type, used only inside this file to form the diagonal height-parity matrix.

Equations

• TauCeti.geckIndexDecidableEq = Classical.decEq ι

The height-parity involution

The signed Chevalley involution

noncomputable def TauCeti.geckChevalleyInvolution {ι : Type u} {R : Type v} {M : Type w} {N : Type u_1} [Fintype ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) : ↥(RootPairing.GeckConstruction.lieAlgebra b) ≃ₗ⁅R⁆ ↥(RootPairing.GeckConstruction.lieAlgebra b)

The Chevalley involution of Geck's matrix Lie algebra. It is the composition of the opposition involution with the height-parity involution, and therefore sends the simple generators by hᵢ ↦ -hᵢ, eᵢ ↦ -fᵢ, and fᵢ ↦ -eᵢ.

Equations

• TauCeti.geckChevalleyInvolution b = (TauCeti.geckOppositionInvolution✝ b).trans (TauCeti.geckHeightInvolution✝ b)

@[simp]

theorem TauCeti.geckChevalleyInvolution_h {ι : Type u} {R : Type v} {M : Type w} {N : Type u_1} [Fintype ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) (i : ↥b.support) : (geckChevalleyInvolution b) ⟨RootPairing.GeckConstruction.h i, ⋯⟩ = -⟨RootPairing.GeckConstruction.h i, ⋯⟩

The Chevalley involution sends a simple Cartan generator to its negative.

@[simp]

theorem TauCeti.geckChevalleyInvolution_e {ι : Type u} {R : Type v} {M : Type w} {N : Type u_1} [Fintype ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) (i : ↥b.support) : (geckChevalleyInvolution b) ⟨RootPairing.GeckConstruction.e i, ⋯⟩ = -⟨RootPairing.GeckConstruction.f i, ⋯⟩

The Chevalley involution sends a simple raising generator to the negative lowering generator.

@[simp]

theorem TauCeti.geckChevalleyInvolution_f {ι : Type u} {R : Type v} {M : Type w} {N : Type u_1} [Fintype ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) (i : ↥b.support) : (geckChevalleyInvolution b) ⟨RootPairing.GeckConstruction.f i, ⋯⟩ = -⟨RootPairing.GeckConstruction.e i, ⋯⟩

The Chevalley involution sends a simple lowering generator to the negative raising generator.

theorem TauCeti.eq_geckChevalleyInvolution {ι : Type u} {R : Type v} {M : Type w} {N : Type u_1} [Fintype ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) {g : ↥(RootPairing.GeckConstruction.lieAlgebra b) →ₗ⁅R⁆ ↥(RootPairing.GeckConstruction.lieAlgebra b)} (hh : ∀ (i : ↥b.support), g ⟨RootPairing.GeckConstruction.h i, ⋯⟩ = -⟨RootPairing.GeckConstruction.h i, ⋯⟩) (he : ∀ (i : ↥b.support), g ⟨RootPairing.GeckConstruction.e i, ⋯⟩ = -⟨RootPairing.GeckConstruction.f i, ⋯⟩) (hf : ∀ (i : ↥b.support), g ⟨RootPairing.GeckConstruction.f i, ⋯⟩ = -⟨RootPairing.GeckConstruction.e i, ⋯⟩) : g = (geckChevalleyInvolution b).toLieHom

TauCeti.geckChevalleyInvolution is the unique Lie homomorphism with the signed formulas on Geck's simple Cartan, raising, and lowering generators.

@[simp]

theorem TauCeti.geckChevalleyInvolution_geckChevalleyInvolution {ι : Type u} {R : Type v} {M : Type w} {N : Type u_1} [Fintype ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) (x : ↥(RootPairing.GeckConstruction.lieAlgebra b)) : (geckChevalleyInvolution b) ((geckChevalleyInvolution b) x) = x

Applying Geck's Chevalley involution twice returns the original element.

theorem TauCeti.involutive_geckChevalleyInvolution {ι : Type u} {R : Type v} {M : Type w} {N : Type u_1} [Fintype ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) : Function.Involutive ⇑(geckChevalleyInvolution b)

Geck's Chevalley involution is an involution.

@[simp]

theorem TauCeti.geckChevalleyInvolution_symm {ι : Type u} {R : Type v} {M : Type w} {N : Type u_1} [Fintype ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (b : P.Base) : (geckChevalleyInvolution b).symm = geckChevalleyInvolution b

Geck's Chevalley involution is its own inverse.