feat (RootSystem/Hom): endomorphisms and automorphisms of root pairings

[ScottCarnahan]

This PR introduces the root pairing endomorphism monoid and automorphism group, and shows that the representations on weight and coweight spaces are injective.

---

[github-actions[bot]]

PR summary 95994d5017

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Aut + Dual.eval_comp_comp_evalEquiv_eq + Equiv + _root_.RootPairing.End + comp_toLinearMap_eq_iff + coroot_coweightMap_apply + coweightEquiv + coweightEquiv_apply + coweightEquiv_comp_toLin + coweightEquiv_mul + coweightEquiv_one + coweightEquiv_symm_coweightMap + coweightHom_toLinearMap + coweightMap_coweightEquiv_symm + coweightMap_mul + coweightMap_one + dualMap_dualMap_eq_iff + dualMap_dualMap_eq_iff_of_injective + eq_comp_toLinearMap_iff + indexEquiv_mul + indexEquiv_one + instance (P : RootPairing ι R M N) : Group (RootPairing.Equiv P P) + instance (P : RootPairing ι R M N) : Monoid (Hom P P) + instance (P : RootPairing ι R M N) : Monoid (RootPairing.Equiv P P) + inv_coweightMap + inv_indexEquiv + inv_weightMap + mul_eq_comp + reflection + reflection_coweightEquiv + reflection_indexEquiv + reflection_weightEquiv + root_weightMap_apply + symm + toEndUnit + toEndUnit_inv + toEndUnit_val + toHom_comp + toHom_one + weightEquiv + weightEquiv_apply + weightEquiv_comp_toLin + weightEquiv_mul + weightEquiv_one + weightEquiv_symm_weightMap + weightHom_toLinearMap + weightMap_mul + weightMap_one + weightMap_weightEquiv_symm + weight_coweight_transpose_apply ++ comp ++ comp_assoc ++ comp_id ++ coweightHom ++ coweightHom_injective ++ id ++ id_comp ++ weightHom ++ weightHom_injective - Hom.comp - Hom.comp_assoc - Hom.comp_id - Hom.id - Hom.id_comp - Hom.reflection

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib-bors[bot]]

:v: ScottCarnahan can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ScottCarnahan]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build