The Weyl group of a rank-two root system is dihedral #

A base with two simple roots presents its Weyl group by two generators: the two simple reflections generate it (TauCeti.weylGroup_eq_closure_simple), they are involutions, and the order of their product is the corresponding entry of the Coxeter matrix of the base (RootPairing.weylGroup.orderOf_ofIdx_mul_ofIdx_eq_coxeterMatrixOfBase). That is exactly the input of TauCeti.nonempty_dihedralGroup_mulEquiv, so the Weyl group is the dihedral group of order twice that entry — and, unlike the presentation of the Weyl group in general, this needs no completeness statement for the braid relations, since in rank two there is only one of them.

Reading the entry off the Cartan type — TauCeti.coxeterMatrixOfBase_eq_six_of_hasCartanType_G2 and its two companions — turns this into the three rank-two cases. The Weyl groups of the types A₂, B₂ and G₂ are the dihedral groups of orders 6, 8 and 12, the last of these being the Weyl-group clause of the G₂ worked example of the root-systems roadmap.

Main results #

TauCeti.nonempty_dihedralGroup_mulEquiv_weylGroup: the Weyl group of a base with two simple roots is the dihedral group of order twice the Coxeter entry of its two simple roots, and TauCeti.card_weylGroup_of_card_support_eq_two is its order.
TauCeti.nonempty_dihedralGroup_mulEquiv_weylGroup_of_hasCartanType_G2: a root system of type G₂ has Weyl group the dihedral group of order 12, with TauCeti.card_weylGroup_of_hasCartanType_G2 its order; the same for types A₂ and B₂.

References #

This file proves the Weyl-group clause of the G₂ worked example of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md ("its Weyl group is the dihedral group of order 12, P.weylGroup ≃* DihedralGroup 6"), together with the two other rank-two types. The computation is the one in N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI §1.3, and J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §9.

Two simple reflections generating the Weyl group #

source

theorem TauCeti.closure_pair_ofIdx_eq_top {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) (hb : b.support.card = 2) {i j : ↥b.support} (hij : i ≠ j) :

Subgroup.closure {RootPairing.weylGroup.ofIdx P ↑i, RootPairing.weylGroup.ofIdx P ↑j} = ⊤

With two simple roots the two corresponding simple reflections generate the Weyl group.

The dihedral structure #

source

theorem TauCeti.nonempty_dihedralGroup_mulEquiv_weylGroup {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) (hb : b.support.card = 2) {i j : ↥b.support} (hij : i ≠ j) :

Nonempty (DihedralGroup ((coxeterMatrixOfBase P b).M i j) ≃* ↥P.weylGroup)

The Weyl group of a base with two simple roots is dihedral. Its order is twice the entry of the Coxeter matrix of the base at the two simple roots, which is the order of the product of the two simple reflections.

Only rank two is available this cheaply. In higher rank the braid relations still hold, but that they present the Weyl group is the Coxeter-presentation theorem, which is not proved here; in rank two the single braid relation is the whole presentation.

source

theorem TauCeti.card_weylGroup_of_card_support_eq_two {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) (hb : b.support.card = 2) {i j : ↥b.support} (hij : i ≠ j) :

Nat.card ↥P.weylGroup = 2 * (coxeterMatrixOfBase P b).M i j

The Weyl group of a base with two simple roots has order twice the Coxeter entry of those two roots, read through DihedralGroup.nat_card.

The three rank-two Cartan types #

source

theorem TauCeti.nonempty_dihedralGroup_mulEquiv_weylGroup_of_hasCartanType_A_two {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) (h : HasCartanType P b (DynkinType.A 2)) :

Nonempty (DihedralGroup 3 ≃* ↥P.weylGroup)

A root system of type A₂ has Weyl group the symmetric group on three letters, in the guise of the dihedral group of order 6.

source

theorem TauCeti.nonempty_dihedralGroup_mulEquiv_weylGroup_of_hasCartanType_B_two {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) (h : HasCartanType P b (DynkinType.B 2)) :

Nonempty (DihedralGroup 4 ≃* ↥P.weylGroup)

A root system of type B₂ has Weyl group the dihedral group of order 8.

source

theorem TauCeti.nonempty_dihedralGroup_mulEquiv_weylGroup_of_hasCartanType_G2 {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (b : P.Base) (h : HasCartanType P b DynkinType.G2) :

Nonempty (DihedralGroup 6 ≃* ↥P.weylGroup)

A root system of type G₂ has Weyl group the dihedral group of order 12. This is the Weyl-group clause of the G₂ worked example of the root-systems roadmap.

source