The Weyl group of a root pairing

This file defines the Weyl group of a root pairing as the subgroup of automorphisms generated by reflection automorphisms. This deviates from the existing literature, which typically defines the Weyl group as the subgroup of linear transformations of the weight space generated by linear reflections. However, the automorphism group of a root pairing comes with a permutation representation on the set indexing roots and faithful linear representations on the weight space and coweight space. Thus, our formalism gives us an isomorphism to the traditional Weyl group together with the natural dual representation generated by coreflections and the permutation representation on roots.

Main definitions

• RootPairing.weylGroup : The group of automorphisms generated by reflections.
• RootPairing.weylGroupToPerm : The permutation representation of the Weyl group on roots.

Results

• RootPairing.range_weylGroup_weightHom : The image of the weight space representation is equal to the subgroup generated by linear reflections.
• RootPairing.range_weylGroup_coweightHom : The image of the coweight space representation is equal to the subgroup generated by linear coreflections.
• RootPairing.range_weylGroupToPerm : The image of the permutation representation is equal to the subgroup generated by reflection permutations.

TODO

• faithfulness of weylGroupToPerm when multiplication by 2 is injective on the weight space.

def RootPairing.weylGroup {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : Subgroup P.Aut

The Weyl group of a root pairing is the group of automorphisms of the root pairing generated by reflections.

Equations

• P.weylGroup = Subgroup.closure (Set.range (RootPairing.Equiv.reflection P))

theorem RootPairing.reflection_mem_weylGroup {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) : RootPairing.Equiv.reflection P i ∈ P.weylGroup

theorem RootPairing.range_weylGroup_weightHom {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : ((RootPairing.Equiv.weightHom P).restrict P.weylGroup).range = Subgroup.closure (Set.range P.reflection)

theorem RootPairing.range_weylGroup_coweightHom {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : ((RootPairing.Equiv.coweightHom P).restrict P.weylGroup).range = Subgroup.closure (Set.range (MulOpposite.op ∘ P.coreflection))

@[reducible, inline]

abbrev RootPairing.weylGroupToPerm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : ↥P.weylGroup →* ι ≃ ι

The permutation representation of the Weyl group induced by reflection_perm.

Equations

• P.weylGroupToPerm = (RootPairing.Equiv.indexHom P).restrict P.weylGroup

theorem RootPairing.range_weylGroupToPerm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : P.weylGroupToPerm.range = Subgroup.closure (Set.range P.reflection_perm)