Weyl words in the Geck carrier

For a valid Dynkin type, the numbered raising and lowering generators in the Geck carrier form an sl₂ pair at every Bourbaki node. The usual product

nᵢ = xᵢ(1) x₋ᵢ(-1) xᵢ(1)

therefore gives a point of the carrier which normalizes its represented weight torus and acts on that torus by the corresponding simple reflection. This file specializes the general Kostant toral-closure construction to the pinned Geck data and multiplies the resulting representatives along a word in the simple reflections.

The construction is deliberately indexed by words, not by Weyl-group elements: proving that two words representing the same Weyl element induce the same torus action is a root-datum calculation, while equality of their carrier representatives is false without accounting for the torus kernel. The word-level representative is the input needed to transport the numbered simple root subgroups to nonsimple roots and to construct the normalizer-to-Weyl-group comparison.

Main declarations

• TauCeti.DynkinType.geckSimpleWeylPoint: the pinned representative attached to one Bourbaki node.
• TauCeti.DynkinType.geckWeylWordPoint: the product of the pinned representatives along a word.
• TauCeti.DynkinType.geckWeylWordTorusAction: the corresponding composite of simple reflections on split-torus points.
• TauCeti.DynkinType.geckWeylWordPoint_conj_geckWeightTorusPoints: conjugation by the word representative realizes that composite action.
• TauCeti.DynkinType.geckWeylWordPoint_mem_normalizer_geckWeightTorusPoints: every word representative normalizes the represented torus.

References

• R. W. Carter, Simple Groups of Lie Type, §§6.4 and 7.2.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• R. Steinberg, Lectures on Chevalley Groups, §3.

A simple Weyl representative

theorem TauCeti.DynkinType.isSl2Triple_geckRepresentation (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : IsSl2Triple ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).h i))) ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator (Sum.inl i)))) ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator (Sum.inr i))))

The defining representation carries the numbered sl₂ triple at node i to an sl₂ triple of endomorphisms of the Geck module.

noncomputable def TauCeti.DynkinType.geckSimpleWeylPoint (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (A : Type v) [CommRing A] : ↥(t.geckPoints ht A)

The pinned simple Weyl representative in the Geck carrier. At node i this is xᵢ(1) x₋ᵢ(-1) xᵢ(1).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.coe_geckSimpleWeylPoint (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (A : Type v) [CommRing A] : ↑(t.geckSimpleWeylPoint ht i A) = (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A (t.geckCoordinateBasisFin ht))).toMulEquiv) (UniversalEnvelopingAlgebra.kostantWeylGL (t.lieBasis ht).rootGenerator (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckCoordinateLattice ht).toAddSubgroup ⋯ ⋯ ⋯ A)

In the Geck coordinate basis, the simple Weyl representative is the integral Weyl automorphism supplied by the corresponding numbered sl₂ pair.

@[simp]

theorem TauCeti.DynkinType.map_geckSimpleWeylPoint (t : DynkinType) (ht : t.Valid) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (i : Fin t.rank) : ((t.geckPointsPresentation ht A).map (t.geckPointsPresentation ht B) f) (t.geckSimpleWeylPoint ht i A) = t.geckSimpleWeylPoint ht i B

The simple Weyl representative is natural in the value ring.

@[simp]

theorem TauCeti.DynkinType.geckSimpleWeylPoint_conj_geckRootSubgroupPoints (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (A : Type v) [CommRing A] (u : A) : t.geckSimpleWeylPoint ht i A * (t.geckRootSubgroupPoints ht (Sum.inl i) A) (Multiplicative.ofAdd u) * (t.geckSimpleWeylPoint ht i A)⁻¹ = (t.geckRootSubgroupPoints ht (Sum.inr i) A) (Multiplicative.ofAdd (-u))

Conjugation by the simple Weyl representative exchanges the raising root subgroup at node i with its lowering root subgroup and negates the parameter.

The action on the represented torus

noncomputable def TauCeti.DynkinType.geckSimpleReflectionTorusPoint (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (A : Type v) [CommRing A] : (Fin t.rank → Aˣ) →* Fin t.rank → Aˣ

The simple reflection at node i, acting on points of the pinned split torus.

Equations

• t.geckSimpleReflectionTorusPoint ht i A = TauCeti.weylReflectTorusPoint ((t.simplyConnectedRootDatum ht).root (t.simpleIndex ht i)) i

theorem TauCeti.DynkinType.geckSimpleReflectionTorusPoint_def (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (A : Type v) [CommRing A] : t.geckSimpleReflectionTorusPoint ht i A = weylReflectTorusPoint ((t.simplyConnectedRootDatum ht).root (t.simpleIndex ht i)) i

The Geck simple reflection on torus points is the multiplicative reflection dual to the corresponding simple-root reflection on characters.

@[simp]

theorem TauCeti.DynkinType.map_geckSimpleReflectionTorusPoint (t : DynkinType) (ht : t.Valid) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (i : Fin t.rank) (s : Fin t.rank → Aˣ) (j : Fin t.rank) : (Units.map ↑f) ((t.geckSimpleReflectionTorusPoint ht i A) s j) = (t.geckSimpleReflectionTorusPoint ht i B) (fun (k : Fin t.rank) => (Units.map ↑f) (s k)) j

The simple reflection on split-torus points is natural in the value ring.

@[simp]

theorem TauCeti.DynkinType.geckSimpleReflectionTorusPoint_geckSimpleReflectionTorusPoint (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (A : Type v) [CommRing A] (s : Fin t.rank → Aˣ) : (t.geckSimpleReflectionTorusPoint ht i A) ((t.geckSimpleReflectionTorusPoint ht i A) s) = s

The Geck simple reflection on split-torus points is an involution.

@[simp]

theorem TauCeti.DynkinType.geckSimpleWeylPoint_conj_geckWeightTorusPoints (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (A : Type v) [CommRing A] (s : Fin t.rank → Aˣ) : t.geckSimpleWeylPoint ht i A * (t.geckWeightTorusPoints ht A) s * (t.geckSimpleWeylPoint ht i A)⁻¹ = (t.geckWeightTorusPoints ht A) ((t.geckSimpleReflectionTorusPoint ht i A) s)

Conjugation by the simple Weyl representative realizes the corresponding reflection on the represented weight torus.

theorem TauCeti.DynkinType.geckSimpleWeylPoint_mem_normalizer_geckWeightTorusPoints (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (A : Type v) [CommRing A] : t.geckSimpleWeylPoint ht i A ∈ Subgroup.normalizer ↑(t.geckWeightTorusPoints ht A).range

Every pinned simple Weyl representative normalizes the represented weight torus.

Products along words

noncomputable def TauCeti.DynkinType.geckWeylWordPoint (t : DynkinType) (ht : t.Valid) (l : List (Fin t.rank)) (A : Type v) [CommRing A] : ↥(t.geckPoints ht A)

The representative in the Geck carrier spelled by a word in the simple reflections.

Equations

• t.geckWeylWordPoint ht l A = (List.map (fun (i : Fin t.rank) => t.geckSimpleWeylPoint ht i A) l).prod

@[simp]

theorem TauCeti.DynkinType.geckWeylWordPoint_nil (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : t.geckWeylWordPoint ht [] A = 1

The empty Weyl word represents the identity point.

@[simp]

theorem TauCeti.DynkinType.geckWeylWordPoint_cons (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (l : List (Fin t.rank)) (A : Type v) [CommRing A] : t.geckWeylWordPoint ht (i :: l) A = t.geckSimpleWeylPoint ht i A * t.geckWeylWordPoint ht l A

Prepending a node multiplies its simple representative on the left.

@[simp]

theorem TauCeti.DynkinType.geckWeylWordPoint_append (t : DynkinType) (ht : t.Valid) (l l' : List (Fin t.rank)) (A : Type v) [CommRing A] : t.geckWeylWordPoint ht (l ++ l') A = t.geckWeylWordPoint ht l A * t.geckWeylWordPoint ht l' A

Concatenation of Weyl words corresponds to multiplication of their representatives.

@[simp]

theorem TauCeti.DynkinType.map_geckWeylWordPoint (t : DynkinType) (ht : t.Valid) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (l : List (Fin t.rank)) : ((t.geckPointsPresentation ht A).map (t.geckPointsPresentation ht B) f) (t.geckWeylWordPoint ht l A) = t.geckWeylWordPoint ht l B

The Weyl-word representative is natural in the value ring.

noncomputable def TauCeti.DynkinType.geckWeylWordTorusAction (t : DynkinType) (ht : t.Valid) (l : List (Fin t.rank)) (A : Type v) [CommRing A] : (Fin t.rank → Aˣ) →* Fin t.rank → Aˣ

The action on split-torus points spelled by a word in simple reflections. The recursion has the same multiplication order as geckWeylWordPoint: the head reflection acts last on the parameter obtained from the tail when the corresponding product acts by conjugation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.geckWeylWordTorusAction_nil (t : DynkinType) (ht : t.Valid) (A : Type v) [CommRing A] : t.geckWeylWordTorusAction ht [] A = MonoidHom.id (Fin t.rank → Aˣ)

The empty word acts identically on split-torus points.

@[simp]

theorem TauCeti.DynkinType.geckWeylWordTorusAction_cons (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (l : List (Fin t.rank)) (A : Type v) [CommRing A] : t.geckWeylWordTorusAction ht (i :: l) A = (t.geckSimpleReflectionTorusPoint ht i A).comp (t.geckWeylWordTorusAction ht l A)

Prepending a node composes its simple reflection on the left.

@[simp]

theorem TauCeti.DynkinType.geckWeylWordTorusAction_append (t : DynkinType) (ht : t.Valid) (l l' : List (Fin t.rank)) (A : Type v) [CommRing A] : t.geckWeylWordTorusAction ht (l ++ l') A = (t.geckWeylWordTorusAction ht l A).comp (t.geckWeylWordTorusAction ht l' A)

Concatenation of words corresponds to composition of their torus actions.

@[simp]

theorem TauCeti.DynkinType.map_geckWeylWordTorusAction (t : DynkinType) (ht : t.Valid) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (l : List (Fin t.rank)) (s : Fin t.rank → Aˣ) (j : Fin t.rank) : (Units.map ↑f) ((t.geckWeylWordTorusAction ht l A) s j) = (t.geckWeylWordTorusAction ht l B) (fun (k : Fin t.rank) => (Units.map ↑f) (s k)) j

The torus action of a Weyl word is natural in the value ring.

@[simp]

theorem TauCeti.DynkinType.geckWeylWordPoint_conj_geckWeightTorusPoints (t : DynkinType) (ht : t.Valid) (l : List (Fin t.rank)) (A : Type v) [CommRing A] (s : Fin t.rank → Aˣ) : t.geckWeylWordPoint ht l A * (t.geckWeightTorusPoints ht A) s * (t.geckWeylWordPoint ht l A)⁻¹ = (t.geckWeightTorusPoints ht A) ((t.geckWeylWordTorusAction ht l A) s)

Conjugation by a Weyl-word representative realizes the word's action on the represented weight torus.

theorem TauCeti.DynkinType.geckWeylWordPoint_mem_normalizer_geckWeightTorusPoints (t : DynkinType) (ht : t.Valid) (l : List (Fin t.rank)) (A : Type v) [CommRing A] : t.geckWeylWordPoint ht l A ∈ Subgroup.normalizer ↑(t.geckWeightTorusPoints ht A).range

Every Weyl-word representative normalizes the represented weight torus.