The root system of the pinned rational Lie algebra

This file identifies the rational root system attached to a valid Dynkin type with the Killing root system of its pinned rational Geck Lie algebra. The identification is pinned: on simple roots it follows the common Bourbaki numbering supplied by Fin t.rank. Unlike RootPairing.GeckConstruction.equivRootSystem, which assumes an algebraically closed coefficient field, this construction works over ℚ by using the rational splitting and distinguished basis already established for the pinned Lie algebra.

Through this identification the roots of the Lie algebra, its nonzero weights, are numbered by the root indices of TauCeti.DynkinType.simplyConnectedRootDatum, so that root vectors, structure constants and root subgroups can all be indexed by the one enumeration of the roots fixed there. The general theory of normalized root-vector systems indexes its families by all weights, the zero weight included, so the file also translates a family indexed by the root numbers into that form.

Main declarations

• TauCeti.DynkinType.rationalRootSystemEquiv: the pinned equivalence from the rational root system to the Killing root system of the rational Lie algebra.
• TauCeti.DynkinType.rootEquiv: the resulting enumeration of the roots of the rational Lie algebra by the root indices Fin t.numRoots of the pinned root datum.
• TauCeti.DynkinType.rootEquiv_apply_cartanBasis and TauCeti.DynkinType.coe_rootEquiv_eq_iff: the root numbered α takes the values of root α of the pinned datum on the Cartan generators, and is characterized by them.
• TauCeti.DynkinType.rootEquiv_simpleIndex, TauCeti.DynkinType.rootEquiv_reflectionPerm_self and TauCeti.DynkinType.rootEquiv_reflectionPerm: the enumeration matches the numbered simple roots and commutes with negation and with reflections.
• TauCeti.DynkinType.coe_rootEquiv_eq_add: the enumeration carries sums of roots of the rational root system to sums of weights.
• TauCeti.DynkinType.coe_rootEquiv_eq_add_iff: a weight sum of enumerated roots is an enumerated root exactly when the corresponding sum holds in the pinned integral datum.
• TauCeti.DynkinType.coe_rootEquiv_add_eq_zero_iff: two enumerated roots are opposite exactly when they are opposite in the pinned integral datum.
• TauCeti.DynkinType.chainBotCoeff_rootEquiv: at a root sum, the descending root-string coefficient of the Lie weights is that of the pinned integral datum.
• TauCeti.DynkinType.extendRootFamily: a family of vectors indexed by the root numbers, extended by 0 to the weight-indexed family that TauCeti.IsSl2System and TauCeti.IsChevalleySystem take.
• TauCeti.DynkinType.isSl2System_extendRootFamily_iff and TauCeti.DynkinType.isChevalleySystem_extendRootFamily_iff: the two conditions read in the root numbering.

noncomputable def TauCeti.DynkinType.rationalRootSystemEquiv (t : DynkinType) (ht : t.Valid) : (t.rationalRootSystem ht).Equiv (LieAlgebra.IsKilling.rootSystem (t.cartanSubalgebra ht))

The pinned rational root system is equivalent to the Killing root system of the pinned rational Lie algebra. The equivalence sends each rational simple root to the root attached to the correspondingly numbered generator of the distinguished Lie-algebra basis.

The pinned enumeration of the roots

noncomputable def TauCeti.DynkinType.rootEquiv (t : DynkinType) (ht : t.Valid) : Fin t.numRoots ≃ ↥LieSubalgebra.root

The pinned enumeration of the roots of the rational Lie algebra. The roots of TauCeti.DynkinType.lieAlgebra are its nonzero weights for the distinguished Cartan subalgebra, collected in LieSubalgebra.root. This is their bijection with the root indices Fin t.numRoots of TauCeti.DynkinType.simplyConnectedRootDatum, carried by TauCeti.DynkinType.rationalRootSystemEquiv; no second enumeration of the roots is introduced.

theorem TauCeti.DynkinType.rootEquiv_eq_indexEquiv (t : DynkinType) (ht : t.Valid) : t.rootEquiv ht = (↑(t.rationalRootSystemEquiv ht)).indexEquiv

The root enumeration is the index bijection of the pinned root-system equivalence. Rewriting with this equation makes the general RootPairing.Hom API available for the enumeration.

@[simp]

theorem TauCeti.DynkinType.rootEquiv_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (t.rootEquiv ht) (t.simpleIndex ht i) = ↑((t.lieBasis ht).baseSupportEquiv i)

The enumeration, the index bijection of the pinned root-system equivalence, sends a Bourbaki-numbered simple root to the simple root of the correspondingly numbered Chevalley generator.

@[simp]

theorem TauCeti.DynkinType.rationalRootSystemEquiv_weightMap_root_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (↑(t.rationalRootSystemEquiv ht)).weightMap ((t.rationalRootSystem ht).root (t.simpleIndex ht i)) = (LieAlgebra.IsKilling.rootSystem (t.cartanSubalgebra ht)).root ↑((t.lieBasis ht).baseSupportEquiv i)

On a Bourbaki-numbered simple root, the weight equivalence lands at the simple Killing root of the correspondingly numbered Lie-algebra generator.

@[simp]

theorem TauCeti.DynkinType.rationalRootSystemEquiv_coweightEquiv_symm_coroot_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (t.rationalRootSystemEquiv ht).coweightEquiv.symm ((t.rationalRootSystem ht).coroot (t.simpleIndex ht i)) = (LieAlgebra.IsKilling.rootSystem (t.cartanSubalgebra ht)).coroot ↑((t.lieBasis ht).baseSupportEquiv i)

On a Bourbaki-numbered simple coroot, the covariant inverse coweight equivalence lands at the simple Killing coroot of the correspondingly numbered Lie-algebra generator.

@[simp]

theorem TauCeti.DynkinType.rootEquiv_apply_cartanBasis (t : DynkinType) (ht : t.Valid) (α : Fin t.numRoots) (i : Fin t.rank) : ↑((t.rootEquiv ht) α) ((t.cartanBasis ht) i) = ↑((t.simplyConnectedRootDatum ht).root α i)

The enumerated roots are the roots of the pinned root datum. Root number α takes the value ⟨α, αᵢ^∨⟩ on the i-th Cartan generator hᵢ = αᵢ^∨, which is the i-th coordinate of α in TauCeti.DynkinType.simplyConnectedRootDatum, written against the fundamental weights.

theorem TauCeti.DynkinType.coe_rootEquiv_eq_iff (t : DynkinType) (ht : t.Valid) {α : Fin t.numRoots} {χ : LieModule.Weight ℚ ↥(t.cartanSubalgebra ht) ↥(t.lieAlgebra ht)} : ↑((t.rootEquiv ht) α) = χ ↔ ∀ (i : Fin t.rank), χ ((t.cartanBasis ht) i) = ↑((t.simplyConnectedRootDatum ht).root α i)

A weight is the root with a given number exactly when it takes the values of that root of the pinned datum on the Cartan generators. The Cartan generators are a basis of the Cartan subalgebra, so this characterizes the enumeration completely.

theorem TauCeti.DynkinType.coe_rootEquiv_eq_add (t : DynkinType) (ht : t.Valid) {α β γ : Fin t.numRoots} (h : (t.rationalRootSystem ht).root γ = (t.rationalRootSystem ht).root α + (t.rationalRootSystem ht).root β) : ⇑↑((t.rootEquiv ht) γ) = ⇑↑((t.rootEquiv ht) α) + ⇑↑((t.rootEquiv ht) β)

The enumeration is additive: when root γ of the rational root system is the sum of roots α and β, the root numbered γ of the Lie algebra is the sum of those numbered α and β.

theorem TauCeti.DynkinType.coe_rootEquiv_eq_add_iff {t : DynkinType} {ht : t.Valid} {α β γ : Fin t.numRoots} : ⇑↑((t.rootEquiv ht) γ) = ⇑↑((t.rootEquiv ht) α) + ⇑↑((t.rootEquiv ht) β) ↔ (t.simplyConnectedRootDatum ht).root γ = (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β

Root sums in the root numbering. The root numbered γ of the rational Lie algebra is the sum of those numbered α and β exactly when root γ of the pinned integral datum is the sum of roots α and β.

theorem TauCeti.DynkinType.chainBotCoeff_rootEquiv {t : DynkinType} {ht : t.Valid} {α β : Fin t.numRoots} (h : (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β ∈ Set.range ⇑(t.simplyConnectedRootDatum ht).root) : LieModule.chainBotCoeff ⇑↑((t.rootEquiv ht) α) ↑((t.rootEquiv ht) β) = RootPairing.chainBotCoeff α β

Root strings in the root numbering. If α + β is a root of the pinned integral datum, the number of times the Lie weight numbered α can be subtracted from the one numbered β and remain a weight is the descending root-string coefficient chainBotCoeff α β of the datum.

@[simp]

theorem TauCeti.DynkinType.rootEquiv_reflectionPerm_self (t : DynkinType) (ht : t.Valid) (α : Fin t.numRoots) : (t.rootEquiv ht) (((t.simplyConnectedRootDatum ht).reflectionPerm α) α) = -(t.rootEquiv ht) α

The enumeration commutes with negation: the root indexed by the reflection of α in itself, which is the index of -α in the pinned datum, is the negative of the root indexed by α.

theorem TauCeti.DynkinType.rootEquiv_reflectionPerm (t : DynkinType) (ht : t.Valid) (α β : Fin t.numRoots) : (t.rootEquiv ht) (((t.simplyConnectedRootDatum ht).reflectionPerm α) β) = ((LieAlgebra.IsKilling.rootSystem (t.cartanSubalgebra ht)).reflectionPerm ((t.rootEquiv ht) α)) ((t.rootEquiv ht) β)

The enumeration commutes with reflections: the root numbered by the reflection of β in α in the pinned datum is the reflection, in the Killing root system, of the root numbered β in the root numbered α.

theorem TauCeti.DynkinType.coe_rootEquiv_add_eq_zero_iff {t : DynkinType} {ht : t.Valid} {α β : Fin t.numRoots} : ⇑↑((t.rootEquiv ht) α) + ⇑↑((t.rootEquiv ht) β) = 0 ↔ (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β = 0

Opposite roots in the root numbering. The weights numbered α and β of the rational Lie algebra sum to zero exactly when roots α and β of the pinned integral datum do.

theorem TauCeti.DynkinType.lieBasis_e_mem_rootSpace_rootEquiv (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (t.lieBasis ht).e i ∈ LieAlgebra.rootSpace (t.cartanSubalgebra ht) ⇑↑((t.rootEquiv ht) (t.simpleIndex ht i))

The numbered raising generator eᵢ is a root vector for the enumerated simple root αᵢ.

theorem TauCeti.DynkinType.lieBasis_f_mem_rootSpace_rootEquiv (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : (t.lieBasis ht).f i ∈ LieAlgebra.rootSpace (t.cartanSubalgebra ht) (-⇑↑((t.rootEquiv ht) (t.simpleIndex ht i)))

The numbered lowering generator fᵢ is a root vector for the negative of the enumerated simple root αᵢ.

theorem TauCeti.DynkinType.exists_coe_rootEquiv_eq (t : DynkinType) (ht : t.Valid) {χ : LieModule.Weight ℚ ↥(t.cartanSubalgebra ht) ↥(t.lieAlgebra ht)} (hχ : χ.IsNonZero) : ∃ (α : Fin t.numRoots), ↑((t.rootEquiv ht) α) = χ

Every root of the rational Lie algebra is enumerated.

Root-indexed families of root vectors

TauCeti.IsSl2System and TauCeti.IsChevalleySystem are stated for families indexed by all weights of the Cartan subalgebra, including the zero weight, where they ask for the value 0. A family indexed by the pinned root numbering is turned into such a family by TauCeti.DynkinType.extendRootFamily, and the two conditions are restated in that numbering.

noncomputable def TauCeti.DynkinType.extendRootFamily {t : DynkinType} {ht : t.Valid} (x : Fin t.numRoots → ↥(t.lieAlgebra ht)) : LieModule.Weight ℚ ↥(t.cartanSubalgebra ht) ↥(t.lieAlgebra ht) → ↥(t.lieAlgebra ht)

The weight-indexed family of a root-indexed family. It takes the value x α at the root numbered α and the value 0 at the zero weight, which is the value TauCeti.IsSl2System prescribes there.

@[simp]

theorem TauCeti.DynkinType.extendRootFamily_rootEquiv {t : DynkinType} {ht : t.Valid} (x : Fin t.numRoots → ↥(t.lieAlgebra ht)) (α : Fin t.numRoots) : extendRootFamily x ↑((t.rootEquiv ht) α) = x α

The extended family takes the value x α at the root numbered α.

@[simp]

theorem TauCeti.DynkinType.extendRootFamily_neg_rootEquiv {t : DynkinType} {ht : t.Valid} (x : Fin t.numRoots → ↥(t.lieAlgebra ht)) (α : Fin t.numRoots) : extendRootFamily x (-↑((t.rootEquiv ht) α)) = x (((t.simplyConnectedRootDatum ht).reflectionPerm α) α)

The extended family takes the value x (-α) at the negative of the root numbered α, where -α is numbered by the reflection of α in itself.

@[simp]

theorem TauCeti.DynkinType.extendRootFamily_of_isZero {t : DynkinType} {ht : t.Valid} (x : Fin t.numRoots → ↥(t.lieAlgebra ht)) {χ : LieModule.Weight ℚ ↥(t.cartanSubalgebra ht) ↥(t.lieAlgebra ht)} (hχ : χ.IsZero) : extendRootFamily x χ = 0

The extended family vanishes at the zero weight.

theorem TauCeti.DynkinType.extendRootFamily_restrict {t : DynkinType} {ht : t.Valid} {y : LieModule.Weight ℚ ↥(t.cartanSubalgebra ht) ↥(t.lieAlgebra ht) → ↥(t.lieAlgebra ht)} (hy : ∀ (χ : LieModule.Weight ℚ ↥(t.cartanSubalgebra ht) ↥(t.lieAlgebra ht)), χ.IsZero → y χ = 0) : (extendRootFamily fun (α : Fin t.numRoots) => y ↑((t.rootEquiv ht) α)) = y

A weight-indexed family vanishing at the zero weight is the extension of its restriction to the enumerated roots.

theorem TauCeti.DynkinType.isSl2System_extendRootFamily_iff {t : DynkinType} {ht : t.Valid} (x : Fin t.numRoots → ↥(t.lieAlgebra ht)) : IsSl2System (extendRootFamily x) ↔ (∀ (α : Fin t.numRoots), x α ∈ LieAlgebra.rootSpace (t.cartanSubalgebra ht) ⇑↑((t.rootEquiv ht) α)) ∧ ∀ (α : Fin t.numRoots), ⁅x α, x (((t.simplyConnectedRootDatum ht).reflectionPerm α) α)⁆ = ↑(LieAlgebra.IsKilling.coroot ↑((t.rootEquiv ht) α))

The sl₂ normalization in the root numbering. The extension of a root-indexed family is a TauCeti.IsSl2System exactly when each x α lies in the root space of the root numbered α and ⁅x α, x (-α)⁆ is the coroot of that root.

theorem TauCeti.DynkinType.isChevalleySystem_extendRootFamily_iff {t : DynkinType} {ht : t.Valid} (ω : ↥(t.lieAlgebra ht) ≃ₗ⁅ℚ⁆ ↥(t.lieAlgebra ht)) (x : Fin t.numRoots → ↥(t.lieAlgebra ht)) : IsChevalleySystem ω (extendRootFamily x) ↔ IsSl2System (extendRootFamily x) ∧ ∀ (α : Fin t.numRoots), ω (x α) = -x (((t.simplyConnectedRootDatum ht).reflectionPerm α) α)

Chevalley systems in the root numbering. The extension of a root-indexed family is a TauCeti.IsChevalleySystem for ω exactly when it is normalized and ω (x α) = -x (-α) for every root number α.