Commit 2024-12-10 06:18 619e1253

View on Github →

refactor(LinearAlgebra/RootSystem): Weyl group (#19744) This PR redefines the Weyl group of a root pairing as the subgroup of automorphisms generated by reflection morphisms. The new definition is isomorphic to the old one, by faithfulness of the weight space representation, but we also get a natural coweight space representation and permutation representation on roots.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

modified theorem RootPairing.IsOrthogonal.symm

deleted theorem RootPairing.exists_root_eq_smul_of_mem_weylGroup

added theorem RootPairing.isOrthogonal_symm

deleted theorem RootPairing.range_weylGroupToPerm

deleted theorem RootPairing.reflection_mem_weylGroup

deleted def RootPairing.weylGroup

deleted def RootPairing.weylGroupToPerm

deleted theorem RootPairing.weylGroupToPerm_apply_reflection

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

added theorem RootPairing.Equiv.coweightEquiv_inv

added theorem RootPairing.Equiv.coweightHom_op

added theorem RootPairing.Equiv.indexEquiv_inv

added def RootPairing.Equiv.indexHom

added theorem RootPairing.Equiv.reflection_inv

added theorem RootPairing.Equiv.weightEquiv_inv

added def RootPairing.Hom.indexHom

Created Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean

added theorem RootPairing.range_weylGroupToPerm

added theorem RootPairing.range_weylGroup_coweightHom

added theorem RootPairing.range_weylGroup_weightHom

added theorem RootPairing.reflection_mem_weylGroup

added def RootPairing.weylGroup