Transporting the Weyl group along an equivalence of root pairings

An equivalence e : P.Equiv Q of root pairings conjugates automorphisms of P into automorphisms of Q (RootPairing.Equiv.autCongr, in TauCeti/LinearAlgebra/RootSystem/EquivComp.lean), and that conjugation carries reflections to reflections: the reflection in the root i goes to the reflection in the root e.indexEquiv i. Since RootPairing.weylGroup is by definition the subgroup of RootPairing.Aut generated by the reflections, conjugation maps it onto the Weyl group of Q, and therefore restricts to a group isomorphism of Weyl groups.

This is what lets a Weyl-group computation performed on one root system be read off on any isomorphic one. Combined with the rigidity half of the Cartan--Killing classification it makes the Weyl group an invariant of the Dynkin type alone; that consequence is drawn in TauCeti/LinearAlgebra/RootSystem/Weyl/CartanType.lean.

Nothing here needs the index sets, the weight spaces or the coweight spaces of the two pairings to agree: e.indexEquiv transports indices, e.weightEquiv transports weight vectors, and the isomorphism of Weyl groups is compatible with both.

Main definitions

• RootPairing.Equiv.weylGroupEquiv: the restriction of conjugation to the Weyl groups, a group isomorphism P.weylGroup ≃* Q.weylGroup.

Main results

• RootPairing.Equiv.autCongr_reflection: conjugation carries the reflection in the root i to the reflection in the root e.indexEquiv i.
• RootPairing.Equiv.map_weylGroup: conjugation maps the Weyl group of P onto that of Q. For Q = P it makes the Weyl group a normal subgroup of the automorphism group (RootPairing.weylGroup_normal).
• RootPairing.Equiv.weylGroupEquiv_ofIdx: the isomorphism of Weyl groups matches up the reflections in the indexed roots along e.indexEquiv.
• RootPairing.Equiv.weylGroupToPerm_weylGroupEquiv: it is equivariant for the permutation actions on root indices, and RootPairing.Equiv.weylGroupEquiv_smul for the actions on weight vectors.
• RootPairing.Equiv.weylGroupEquiv_id and RootPairing.Equiv.weylGroupEquiv_comp: the construction is functorial.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1.

@[simp]

theorem RootPairing.Equiv.autCongr_reflection {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (i : ι) : e.autCongr (reflection P i) = reflection Q ((↑e).indexEquiv i)

Conjugation carries reflections to reflections: the reflection in the root i goes to the reflection in the root e.indexEquiv i.

@[simp]

theorem RootPairing.Equiv.map_weylGroup {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) : Subgroup.map (↑e.autCongr) P.weylGroup = Q.weylGroup

Conjugation maps the Weyl group of P onto the Weyl group of Q.

instance RootPairing.weylGroup_normal {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} : P.weylGroup.Normal

The Weyl group is a normal subgroup of the automorphism group: conjugation by an automorphism g maps the Weyl group onto itself (RootPairing.Equiv.map_weylGroup for e := g).

noncomputable def RootPairing.Equiv.weylGroupEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) : ↥P.weylGroup ≃* ↥Q.weylGroup

The Weyl group transported along an equivalence of root pairings. Conjugation by e restricts to a group isomorphism of Weyl groups.

@[simp]

theorem RootPairing.Equiv.coe_weylGroupEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (w : ↥P.weylGroup) : ↑(e.weylGroupEquiv w) = e.autCongr ↑w

@[simp]

theorem RootPairing.Equiv.coe_weylGroupEquiv_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (w : ↥Q.weylGroup) : ↑(e.weylGroupEquiv.symm w) = e.autCongr.symm ↑w

@[simp]

theorem RootPairing.Equiv.weylGroupEquiv_ofIdx {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (i : ι) : e.weylGroupEquiv (weylGroup.ofIdx P i) = weylGroup.ofIdx Q ((↑e).indexEquiv i)

The isomorphism of Weyl groups matches up the reflections in the indexed roots along e.indexEquiv.

theorem RootPairing.Equiv.weylGroupToPerm_weylGroupEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (w : ↥P.weylGroup) : Q.weylGroupToPerm (e.weylGroupEquiv w) = (↑e).indexEquiv.permCongr (P.weylGroupToPerm w)

The isomorphism of Weyl groups is equivariant for the permutation actions on root indices: the permutation of Q's root indices is the one of P's conjugated by e.indexEquiv.

Not a simp lemma: RootPairing.weylGroupToPerm is a MonoidHom.domRestrict, so MonoidHom.domRestrict_apply, RootPairing.Equiv.coe_weylGroupEquiv and RootPairing.Equiv.indexHom_apply rewrite the left-hand side to (↑(e.autCongr ↑w)).indexEquiv; RootPairing.Equiv.indexEquiv_autCongr_apply is the simp lemma that then finishes the job.

theorem RootPairing.Equiv.weylGroupEquiv_smul {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (e : P.Equiv Q) (w : ↥P.weylGroup) (x : M) : e.weylGroupEquiv w • e.weightEquiv x = e.weightEquiv (w • x)

The isomorphism of Weyl groups is equivariant for the actions on weight vectors.

Not a simp lemma, for the same reason as RootPairing.Equiv.autCongr_smul.

@[simp]

theorem RootPairing.Equiv.weylGroupEquiv_id {ι : Type u_1} {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} : (id P).weylGroupEquiv = MulEquiv.refl ↥P.weylGroup

The Weyl-group isomorphism of the identity equivalence is the identity.

@[simp]

theorem RootPairing.Equiv.weylGroupEquiv_comp {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_5} {N : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} {M₃ : Type u_9} {N₃ : Type u_10} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} {S : RootPairing ι₃ R M₃ N₃} (e : P.Equiv Q) (f : Q.Equiv S) : (f.comp e).weylGroupEquiv = e.weylGroupEquiv.trans f.weylGroupEquiv

The Weyl-group isomorphism of a composite is the composite of the Weyl-group isomorphisms.