Root systems whose automorphisms are all Weyl

An automorphism u of a finite reduced crystallographic root system carries a base b to a base, and the Weyl group acts simply transitively on the bases (RootPairing.Base.existsUnique_map_eq). So u = w v with w in the Weyl group and v carrying b onto itself. Such a v permutes the simple roots of b by a symmetry of the Cartan matrix, and, when the roots span the weight space, v is determined by that permutation. Hence, when the Cartan matrix of b has no nontrivial symmetry, every automorphism lies in the Weyl group.

This is the half of the decomposition Aut(Φ) = W(Φ) ⋊ Aut(Dynkin diagram) needed to identify the full automorphism group of a root system of rigid type, such as E₈, with its Weyl group.

Main results

• RootPairing.Base.eq_one_of_forall_indexEquiv_eq: an automorphism of a root system fixing every simple root of a base is the identity.
• RootPairing.Base.mem_support_map_iff: the simple roots of a transported base.
• RootPairing.Base.weylGroup_eq_top_of_matrixSymmetryGroup_eq_bot: if the Cartan matrix of a base has no nontrivial symmetry, every automorphism lies in the Weyl group.
• TauCeti.HasCartanType.weylGroup_eq_top: the same for a base of a Dynkin type whose diagram has no nontrivial symmetry, and TauCeti.weylGroup_eq_top_of_hasCartanType_E8 its instance for E₈.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1.5, Proposition 16 and §4, Plate VII.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §12.2.

theorem RootPairing.Base.eq_one_of_forall_indexEquiv_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} [P.IsRootSystem] (b : P.Base) {u : P.Aut} (hu : ∀ i ∈ b.support, (↑u).indexEquiv i = i) : u = 1

An automorphism of a root system fixing every simple root of a base is the identity. The simple roots span the root span, which is everything for a root system.

theorem RootPairing.Base.mem_support_map_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} (b : P.Base) (e : P.Aut) (j : ι) : j ∈ (b.map e).support ↔ (↑e).indexEquiv.symm j ∈ b.support

A root index is simple for the transported base b.map e exactly when its preimage under e is simple for b.

theorem RootPairing.Base.weylGroup_eq_top_of_matrixSymmetryGroup_eq_bot {ι : 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 ι] [IsDomain R] [CharZero R] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem] (b : P.Base) (hb : TauCeti.matrixSymmetryGroup b.cartanMatrix = ⊥) : P.weylGroup = ⊤

If the Cartan matrix of a base has no nontrivial symmetry, every automorphism of the root system lies in the Weyl group.

theorem TauCeti.HasCartanType.weylGroup_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 ι] [IsDomain R] [CharZero R] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem] {b : P.Base} {t : DynkinType} (h : HasCartanType P b t) (ht : t.diagramSymmetry = ⊥) : P.weylGroup = ⊤

A root system with a base of a Dynkin type whose diagram has no nontrivial symmetry has every automorphism in its Weyl group.

theorem TauCeti.weylGroup_eq_top_of_hasCartanType_E8 {ι : 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 ι] [IsDomain R] [CharZero R] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem] {b : P.Base} (h : HasCartanType P b DynkinType.E8) : P.weylGroup = ⊤

Every automorphism of a root system of type E₈ lies in its Weyl group.