Permutation actions of Weyl groups

This file proves that the action of the automorphism group of a root system on its root indices is faithful. Consequently that automorphism group is itself finite when the root index type is finite, and hence so is every subgroup of it, the Weyl group in particular. It also records how that action evaluates on simple reflections, how it interacts with root negation, and the sign change a reflection induces on its own coroot functional. Alongside it, the weight-space action of the Weyl group is faithful, with no spanning hypothesis needed. More generally, an automorphism transports coroot functionals along its action on weights, matching the coroot functional of a root with that of its image.

Main results

• RootPairing.Equiv.indexHom_injective says that an automorphism of a root system is determined by its permutation of the roots.
• RootPairing.Equiv.indexHom_injective_of_corootSpan_eq_top gives the same faithfulness when the coroots span, in particular for simply connected integral root data.
• RootPairing.coroot'_reflection_self says a reflection reverses the sign of its own coroot functional.
• RootPairing.coroot'_smul and RootPairing.coroot'_weylGroupToPerm_smul say an automorphism, and in particular a Weyl-group element, carries the coroot functional of a root to the coroot functional of its image.
• RootPairing.weylGroupToPerm_ofIdx_apply evaluates the action of a simple reflection.
• RootPairing.weylGroupToPerm_neg says the action commutes with root negation.
• RootPairing.weylGroup.ofIdx_mul_self says a simple reflection is an involution.
• RootPairing.weylGroup.ofIdx_ne_one says a simple reflection is not the identity over a ring of characteristic zero.
• RootPairing.weylGroup.eq_one_of_smul_eq_self says a Weyl-group element acting trivially on the weight space is the identity.
• RootPairing.weylGroup.ext says two Weyl-group elements agreeing on the weight space are equal.
• RootPairing.weylGroup.ofIdx_weylGroupToPerm_eq_conj says that conjugating a simple reflection by a Weyl-group element gives the reflection in the image root index.
• RootPairing.weylGroup.commute_ofIdx_of_isOrthogonal says orthogonal roots have commuting reflections.
• RootPairing.finite_aut proves that the automorphism group of a finite root system is finite, and RootPairing.finite_subgroup_aut deduces the same for every subgroup of it.
• RootPairing.finite_weylGroup is the resulting finiteness theorem for the Weyl group.

References

• Root systems roadmap

theorem RootPairing.Equiv.indexHom_injective_of_span_eq_top {ι : 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) (hspan : Submodule.span R (Set.range ⇑P.root) = ⊤) : Function.Injective ⇑(indexHom P)

If the roots span, an automorphism of a root pairing is determined by its permutation of the root indices.

theorem RootPairing.Equiv.indexHom_injective_of_corootSpan_eq_top {ι : 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) (hspan : P.corootSpan R = ⊤) : Function.Injective ⇑(indexHom P)

If the coroots span, an automorphism of a root pairing is determined by its permutation of the root indices. This applies to simply connected root data over the integers.

theorem RootPairing.Equiv.indexHom_injective {ι : 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.IsRootSystem] : Function.Injective ⇑(indexHom P)

An automorphism of a root system is determined by its permutation of the root indices.

@[simp]

theorem RootPairing.coroot'_reflectionPerm_self {ι : 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 : ι) : P.coroot' ((P.reflectionPerm i) i) = -P.coroot' i

Reflecting a root in itself negates its coroot functional.

theorem RootPairing.coroot'_reflection_self {ι : 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 : ι) (x : M) : (P.coroot' i) ((P.reflection i) x) = -(P.coroot' i) x

A reflection reverses the sign of its own coroot functional.

theorem RootPairing.coroot'_smul {ι : 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) (g : P.Aut) (i : ι) (x : M) : (P.coroot' i) (g • x) = (P.coroot' ((↑g).indexEquiv.symm i)) x

An automorphism of a root pairing transports coroot functionals along its action on weights.

theorem RootPairing.coroot'_weylGroupToPerm_smul {ι : 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) (w : ↥P.weylGroup) (i : ι) (x : M) : (P.coroot' ((P.weylGroupToPerm w) i)) (w • x) = (P.coroot' i) x

A Weyl-group element matches the coroot functional of a root with the coroot functional of its image.

theorem RootPairing.weylGroupToPerm_injective_of_span_eq_top {ι : 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) (hspan : Submodule.span R (Set.range ⇑P.root) = ⊤) : Function.Injective ⇑P.weylGroupToPerm

If the roots span, the action of the Weyl group on root indices is faithful.

theorem RootPairing.weylGroupToPerm_injective {ι : 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.IsRootSystem] : Function.Injective ⇑P.weylGroupToPerm

The action of the Weyl group on root indices is faithful.

theorem RootPairing.weylGroupToPerm_ofIdx_apply {ι : 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 j : ι) : (P.weylGroupToPerm (weylGroup.ofIdx P i)) j = (P.reflectionPerm i) j

The Weyl-group permutation of a simple reflection is the corresponding root-index reflection.

theorem RootPairing.weylGroupToPerm_mul_ofIdx_apply {ι : 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) (w : ↥P.weylGroup) (i j : ι) : (P.weylGroupToPerm (w * weylGroup.ofIdx P i)) j = (P.weylGroupToPerm w) ((P.reflectionPerm i) j)

Right multiplication by a simple reflection acts by first reflecting the root index.

theorem RootPairing.weylGroupToPerm_ofIdx_mul_apply {ι : 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) (w : ↥P.weylGroup) (i j : ι) : (P.weylGroupToPerm (weylGroup.ofIdx P i * w)) j = (P.reflectionPerm i) ((P.weylGroupToPerm w) j)

Left multiplication by a simple reflection acts by reflecting the resulting root index.

theorem RootPairing.weylGroupToPerm_neg {ι : 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) (w : ↥P.weylGroup) (j : ι) : (P.weylGroupToPerm w) (-j) = -(P.weylGroupToPerm w) j

The Weyl-group action on root indices commutes with root negation.

@[simp]

theorem RootPairing.weylGroup.coe_ofIdx {ι : 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 : ι) : ↑(ofIdx P i) = Equiv.reflection P i

A simple reflection of the Weyl group is the corresponding reflection of the root pairing.

@[simp]

theorem RootPairing.weylGroup.ofIdx_inv_eq {ι : 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 : ι) : (ofIdx P i)⁻¹ = ofIdx P i

A simple reflection of the Weyl group is its own inverse.

@[simp]

theorem RootPairing.weylGroup.ofIdx_mul_self {ι : 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 : ι) : ofIdx P i * ofIdx P i = 1

A simple reflection of the Weyl group is an involution.

theorem RootPairing.weylGroup.ofIdx_ne_one {ι : 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) [CharZero R] (i : ι) : ofIdx P i ≠ 1

A simple reflection is not the identity over a ring of characteristic zero.

theorem RootPairing.weylGroup.eq_one_of_smul_eq_self {ι : 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} {w : ↥P.weylGroup} (h : ∀ (x : M), w • x = x) : w = 1

A Weyl-group element acting trivially on the weight space is the identity: the weight-space representation of the automorphism group of a root pairing is faithful.

theorem RootPairing.weylGroup.ext {ι : 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} {v w : ↥P.weylGroup} (h : ∀ (x : M), v • x = w • x) : v = w

Two Weyl-group elements agreeing on the weight space are equal.

theorem RootPairing.weylGroup.ext_iff {ι : 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} {v w : ↥P.weylGroup} : v = w ↔ ∀ (x : M), v • x = w • x

theorem RootPairing.weylGroup.ofIdx_weylGroupToPerm_eq_conj {ι : 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) (w : ↥P.weylGroup) (i : ι) : ofIdx P ((P.weylGroupToPerm w) i) = w * ofIdx P i * w⁻¹

Conjugating a simple reflection transports it along the permutation action: the reflection in the image of a root index is the conjugate of the reflection in that root index.

theorem RootPairing.weylGroup.commute_ofIdx_of_isOrthogonal {ι : 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 j : ι} (h : P.IsOrthogonal i j) : Commute (ofIdx P i) (ofIdx P j)

Orthogonal roots have commuting reflections in the Weyl group.

theorem RootPairing.finite_aut_of_span_eq_top {ι : 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) [Finite ι] (hspan : Submodule.span R (Set.range ⇑P.root) = ⊤) : Finite P.Aut

If the roots span, the automorphism group is finite when the root index type is finite.

theorem RootPairing.finite_aut {ι : 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) [Finite ι] [P.IsRootSystem] : Finite P.Aut

The automorphism group of a finite root system is finite.

theorem RootPairing.finite_subgroup_aut_of_span_eq_top {ι : 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) [Finite ι] (hspan : Submodule.span R (Set.range ⇑P.root) = ⊤) (G : Subgroup P.Aut) : Finite ↥G

If the roots span, every subgroup of the automorphism group is finite when the root index type is finite.

theorem RootPairing.finite_subgroup_aut {ι : 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) [Finite ι] [P.IsRootSystem] (G : Subgroup P.Aut) : Finite ↥G

Every subgroup of the automorphism group of a finite root system is finite.

theorem RootPairing.card_aut_le_factorial_of_span_eq_top {ι : 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) [Finite ι] (hspan : Submodule.span R (Set.range ⇑P.root) = ⊤) : Nat.card P.Aut ≤ (Nat.card ι).factorial

If the roots span, the automorphism group has order at most the factorial of the number of roots.

theorem RootPairing.card_aut_le_factorial {ι : 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) [Finite ι] [P.IsRootSystem] : Nat.card P.Aut ≤ (Nat.card ι).factorial

The automorphism group of a finite root system has order at most the factorial of the number of roots.

theorem RootPairing.card_subgroup_aut_le_factorial_of_span_eq_top {ι : 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) [Finite ι] (hspan : Submodule.span R (Set.range ⇑P.root) = ⊤) (G : Subgroup P.Aut) : Nat.card ↥G ≤ (Nat.card ι).factorial

If the roots span, every subgroup of the automorphism group has order at most the factorial of the number of roots.

theorem RootPairing.card_subgroup_aut_le_factorial {ι : 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) [Finite ι] [P.IsRootSystem] (G : Subgroup P.Aut) : Nat.card ↥G ≤ (Nat.card ι).factorial

Every subgroup of the automorphism group of a finite root system has order at most the factorial of the number of roots.

theorem RootPairing.finite_weylGroup_of_span_eq_top {ι : 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) [Finite ι] (hspan : Submodule.span R (Set.range ⇑P.root) = ⊤) : Finite ↥P.weylGroup

If the roots span, the Weyl group is finite when the root index type is finite.

theorem RootPairing.finite_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) [Finite ι] [P.IsRootSystem] : Finite ↥P.weylGroup

The Weyl group of a finite root system is finite.

theorem RootPairing.card_weylGroup_le_factorial_of_span_eq_top {ι : 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) [Finite ι] (hspan : Submodule.span R (Set.range ⇑P.root) = ⊤) : Nat.card ↥P.weylGroup ≤ (Nat.card ι).factorial

If the roots span, the order of the Weyl group is at most the factorial of the number of roots.

theorem RootPairing.card_weylGroup_le_factorial {ι : 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) [Finite ι] [P.IsRootSystem] : Nat.card ↥P.weylGroup ≤ (Nat.card ι).factorial

The order of the Weyl group of a finite root system is at most the factorial of the number of roots.