Commit 2024-10-31 02:17 169ed0ac

View on Github →

feat (RootSystem/Hom): endomorphisms and automorphisms of root pairings (#18025) This PR introduces the root pairing endomorphism monoid and automorphism group, and shows that the representations on weight and coweight spaces are injective.

Estimated changes

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

added theorem LinearEquiv.comp_toLinearMap_eq_iff

added theorem LinearEquiv.eq_comp_toLinearMap_iff

Modified Mathlib/LinearAlgebra/Dual.lean

added theorem Module.Dual.eval_comp_comp_evalEquiv_eq

added theorem Module.dualMap_dualMap_eq_iff

added theorem Module.dualMap_dualMap_eq_iff_of_injective

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

added def RootPairing.Equiv.comp

added theorem RootPairing.Equiv.comp_assoc

added theorem RootPairing.Equiv.comp_id

added def RootPairing.Equiv.coweightEquiv

added theorem RootPairing.Equiv.coweightEquiv_apply

added theorem RootPairing.Equiv.coweightEquiv_comp_toLin

added theorem RootPairing.Equiv.coweightEquiv_mul

added theorem RootPairing.Equiv.coweightEquiv_one

added theorem RootPairing.Equiv.coweightEquiv_symm_coweightMap

added def RootPairing.Equiv.coweightHom

added theorem RootPairing.Equiv.coweightHom_injective

added theorem RootPairing.Equiv.coweightHom_toLinearMap

added theorem RootPairing.Equiv.coweightMap_coweightEquiv_symm

added def RootPairing.Equiv.id

added theorem RootPairing.Equiv.id_comp

added theorem RootPairing.Equiv.inv_coweightMap

added theorem RootPairing.Equiv.inv_indexEquiv

added theorem RootPairing.Equiv.inv_weightMap

added theorem RootPairing.Equiv.mul_eq_comp

added def RootPairing.Equiv.reflection

added theorem RootPairing.Equiv.reflection_coweightEquiv

added theorem RootPairing.Equiv.reflection_indexEquiv

added theorem RootPairing.Equiv.reflection_weightEquiv

added def RootPairing.Equiv.symm

added def RootPairing.Equiv.toEndUnit

added theorem RootPairing.Equiv.toEndUnit_inv

added theorem RootPairing.Equiv.toEndUnit_val

added theorem RootPairing.Equiv.toHom_comp

added theorem RootPairing.Equiv.toHom_one

added def RootPairing.Equiv.weightEquiv

added theorem RootPairing.Equiv.weightEquiv_apply

added theorem RootPairing.Equiv.weightEquiv_comp_toLin

added theorem RootPairing.Equiv.weightEquiv_mul

added theorem RootPairing.Equiv.weightEquiv_one

added theorem RootPairing.Equiv.weightEquiv_symm_weightMap

added def RootPairing.Equiv.weightHom

added theorem RootPairing.Equiv.weightHom_injective

added theorem RootPairing.Equiv.weightHom_toLinearMap

added theorem RootPairing.Equiv.weightMap_weightEquiv_symm

modified def RootPairing.Hom.comp

modified theorem RootPairing.Hom.comp_assoc

modified theorem RootPairing.Hom.comp_id

added theorem RootPairing.Hom.coroot_coweightMap_apply

added def RootPairing.Hom.coweightHom

added theorem RootPairing.Hom.coweightHom_injective

added theorem RootPairing.Hom.coweightMap_mul

added theorem RootPairing.Hom.coweightMap_one

modified def RootPairing.Hom.id

modified theorem RootPairing.Hom.id_comp

added theorem RootPairing.Hom.indexEquiv_mul

added theorem RootPairing.Hom.indexEquiv_one

deleted def RootPairing.Hom.reflection

added theorem RootPairing.Hom.root_weightMap_apply

added def RootPairing.Hom.weightHom

added theorem RootPairing.Hom.weightHom_injective

added theorem RootPairing.Hom.weightMap_mul

added theorem RootPairing.Hom.weightMap_one

added theorem RootPairing.Hom.weight_coweight_transpose_apply