The Chevalley system of the pinned rational Lie algebra

TauCeti.DynkinType.exists_isChevalleySystem shows that the pinned rational Lie algebra TauCeti.DynkinType.lieAlgebra has a Chevalley system for its signed Chevalley involution ω whose root vectors at ±αᵢ are the Bourbaki-numbered generators eᵢ and fᵢ. Those conditions fix such a system only up to signs at the non-simple roots. This file names one, TauCeti.DynkinType.chevalleySystem, indexed by the root numbers Fin t.numRoots of TauCeti.DynkinType.simplyConnectedRootDatum and written down from Geck's generators, by recursion on the height of a root:

• at a simple root αᵢ it is eᵢ;
• at a positive root γ that is not simple, let i be the least Bourbaki node for which γ - αᵢ is a root β; then it is (r + 1)⁻¹ • ⁅eᵢ, e_β⁆, where r is the largest integer with β - r αᵢ a root;
• at a negative root -γ it is -ω (e_γ).

Compared step by step with any Chevalley system pinned to the generators, through the root-string normalization TauCeti.IsChevalleySystem.inv_smul_lie_eq_or_eq_neg, the named family agrees with it up to a sign that is the same at γ and at -γ. It is therefore itself a Chevalley system for ω, so its structure constants are the integers ±(r + 1) of TauCeti.IsChevalleySystem.intStructureConstant, and it names a root vector for every root, as the Kostant ℤ-form and the root subgroups of non-simple roots require.

Main definitions

• TauCeti.DynkinType.chevalleySystem: the root vector attached to each root number.

Main results

• TauCeti.DynkinType.chevalleySystem_simpleIndex and TauCeti.DynkinType.chevalleySystem_reflectionPerm_simpleIndex: the root vectors at αᵢ and -αᵢ are the numbered generators eᵢ and fᵢ.
• TauCeti.DynkinType.exists_chevalleySystem_eq_inv_smul_lie: the recursion at a positive root that is not simple.
• TauCeti.DynkinType.chevalleyInvolution_chevalleySystem: the Chevalley involution sends the root vector of γ to minus that of -γ.
• TauCeti.DynkinType.isChevalleySystem_chevalleySystem: the family is a Chevalley system for the signed Chevalley involution.
• TauCeti.DynkinType.chevalleySystem_mem_rootSpace and TauCeti.DynkinType.lie_chevalleySystem_reflectionPerm_self: each root vector lies in its root space, and the root vectors of γ and -γ bracket to the coroot of γ.
• TauCeti.DynkinType.lie_lieBasis_h_chevalleySystem: the numbered Cartan generators act on each root vector through the coordinates of its root.
• TauCeti.DynkinType.isSl2Triple_chevalleySystem and TauCeti.DynkinType.isNilpotent_ad_chevalleySystem: the root vectors of γ and -γ span an sl₂ triple with the coroot of γ, and act nilpotently.

References

• R. W. Carter, Simple Groups of Lie Type, §4.2.
• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.

Removing a simple root from a positive root

The named Chevalley system

@[irreducible]

def TauCeti.DynkinType.chevalleySystem (t : DynkinType) (ht : t.Valid) (γ : Fin t.numRoots) : ↥(t.lieAlgebra ht)

The Chevalley system of the pinned rational Lie algebra. The root vector attached to the root numbered γ: the generator eᵢ at a simple root αᵢ; at a positive root γ that is not simple, (r + 1)⁻¹ • ⁅eᵢ, e_β⁆ for i the least Bourbaki node with γ - αᵢ a root β and r the largest integer with β - r αᵢ a root; and -ω (e_{-γ}) at a negative root γ, for ω the signed Chevalley involution.

theorem TauCeti.DynkinType.exists_chevalleySystem_eq_inv_smul_lie {t : DynkinType} {ht : t.Valid} {γ : Fin t.numRoots} (hγ : (t.rationalBase ht).IsPos γ) (hs : γ ∉ (t.rationalBase ht).support) : ∃ (i : Fin t.rank) (β : Fin t.numRoots), (t.rationalRootSystem ht).root γ = (t.rationalRootSystem ht).root (t.simpleIndex ht i) + (t.rationalRootSystem ht).root β ∧ (∀ j < i, ∀ (β' : Fin t.numRoots), (t.rationalRootSystem ht).root γ ≠ (t.rationalRootSystem ht).root (t.simpleIndex ht j) + (t.rationalRootSystem ht).root β') ∧ t.chevalleySystem ht γ = (↑(LieModule.chainBotCoeff ⇑↑((t.rootEquiv ht) (t.simpleIndex ht i)) ↑((t.rootEquiv ht) β) + 1))⁻¹ • ⁅(t.lieBasis ht).e i, t.chevalleySystem ht β⁆

The recursion at a positive root that is not simple. Such a root γ is αᵢ + β for a root β, where i is the least Bourbaki node for which γ - αᵢ is a root, and its root vector is (r + 1)⁻¹ • ⁅eᵢ, e_β⁆, where r is the largest integer with β - r αᵢ a root. Since γ and i determine β, this characterizes the root vector of γ from those of lower height.

@[simp]

theorem TauCeti.DynkinType.chevalleySystem_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : t.chevalleySystem ht (t.simpleIndex ht i) = (t.lieBasis ht).e i

The root vector at a simple root αᵢ is the numbered generator eᵢ.

@[simp]

theorem TauCeti.DynkinType.chevalleyInvolution_chevalleySystem (t : DynkinType) (ht : t.Valid) (γ : Fin t.numRoots) : (t.chevalleyInvolution ht) (t.chevalleySystem ht γ) = -t.chevalleySystem ht (((t.simplyConnectedRootDatum ht).reflectionPerm γ) γ)

The Chevalley involution exchanges opposite root vectors: it sends the root vector of γ to minus that of -γ.

@[simp]

theorem TauCeti.DynkinType.chevalleySystem_reflectionPerm_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : t.chevalleySystem ht (((t.simplyConnectedRootDatum ht).reflectionPerm (t.simpleIndex ht i)) (t.simpleIndex ht i)) = (t.lieBasis ht).f i

The root vector at a negative simple root -αᵢ is the numbered generator fᵢ.

Comparison with a pinned Chevalley system

The sign comparison is carried out for any root-indexed family satisfying the defining equations of TauCeti.DynkinType.chevalleySystem, against the root-indexed family X of a pinned Chevalley system, with the root-string coefficient left abstract.

theorem TauCeti.DynkinType.isChevalleySystem_chevalleySystem (t : DynkinType) (ht : t.Valid) : IsChevalleySystem (t.chevalleyInvolution ht) (extendRootFamily (t.chevalleySystem ht))

The named family is a Chevalley system. Extended by 0 at the zero weight, the root vectors TauCeti.DynkinType.chevalleySystem form a Chevalley system for the signed Chevalley involution of the pinned rational Lie algebra.

theorem TauCeti.DynkinType.chevalleySystem_mem_rootSpace (t : DynkinType) (ht : t.Valid) (γ : Fin t.numRoots) : t.chevalleySystem ht γ ∈ LieAlgebra.rootSpace (t.cartanSubalgebra ht) ⇑↑((t.rootEquiv ht) γ)

Each named root vector lies in the root space of its root.

theorem TauCeti.DynkinType.lie_lieBasis_h_chevalleySystem (t : DynkinType) (ht : t.Valid) (γ : Fin t.numRoots) (j : Fin t.rank) : ⁅(t.lieBasis ht).h j, t.chevalleySystem ht γ⁆ = ↑((t.simplyConnectedRootDatum ht).root γ j) • t.chevalleySystem ht γ

Each named root vector is a weight vector of its root: the numbered Cartan generator hⱼ acts on e_γ by the j-th coordinate of the root γ of the pinned datum.

theorem TauCeti.DynkinType.lie_chevalleySystem_reflectionPerm_self (t : DynkinType) (ht : t.Valid) (γ : Fin t.numRoots) : ⁅t.chevalleySystem ht γ, t.chevalleySystem ht (((t.simplyConnectedRootDatum ht).reflectionPerm γ) γ)⁆ = ↑(LieAlgebra.IsKilling.coroot ↑((t.rootEquiv ht) γ))

The named root vectors of γ and -γ bracket to the coroot of γ.

theorem TauCeti.DynkinType.isSl2Triple_chevalleySystem (t : DynkinType) (ht : t.Valid) (γ : Fin t.numRoots) : IsSl2Triple (↑(LieAlgebra.IsKilling.coroot ↑((t.rootEquiv ht) γ))) (t.chevalleySystem ht γ) (t.chevalleySystem ht (((t.simplyConnectedRootDatum ht).reflectionPerm γ) γ))

The coroot of γ and the named root vectors of γ and -γ form an sl₂ triple.

theorem TauCeti.DynkinType.isNilpotent_ad_chevalleySystem (t : DynkinType) (ht : t.Valid) (γ : Fin t.numRoots) : IsNilpotent ((LieAlgebra.ad ℚ ↥(t.lieAlgebra ht)) (t.chevalleySystem ht γ))

Each named root vector acts nilpotently in the adjoint representation.