Root data and root systems #

This file contains basic definitions for root systems and root data.

Main definitions / results: #

RootPairing: Given two perfectly-paired R-modules M and N (over some commutative ring R) a root pairing with finite indexing set ι is the data of an ι-indexed subset of M ("the roots") and an ι-indexed subset of N ("the coroots") satisfying the axioms familiar from the traditional theory of root systems / data.
RootDatum: A root datum is a root pairing for which the roots and coroots take values in finitely-generated free Abelian groups.
RootSystem: A root system is a root pairing for which the roots span their ambient module.
RootPairing.IsCrystallographic: A root pairing is said to be crystallographic if the pairing between a root and coroot is always an integer.
RootPairing.IsReduced: A root pairing is said to be reduced if it never contains the double of a root.
RootPairing.ext: In characteristic zero if there is no torsion, the correspondence between roots and coroots is unique.
RootSystem.ext: In characteristic zero if there is no torsion, a root system is determined entirely by its roots.
RootSystem.mk': In characteristic zero if there is no torsion, to check that a family of roots form a root system, we do not need to check that the coroots are stable under reflections since this follows from the corresponding property for the roots.

Implementation details #

A root datum is sometimes defined as two subsets: roots and coroots, together with a bijection between them, subject to hypotheses. However the hypotheses ensure that the bijection is unique and so the question arises of whether this bijection should be part of the data of a root datum or whether one should merely assert its existence. For root systems, things are even more extreme: the coroots are uniquely determined by the roots. Furthermore a root system induces a canonical non-degenerate bilinear form on the ambient space and many informal accounts even include this form as part of the data.

We have opted for a design in which some of the uniquely-determined data is included: the bijection between roots and coroots is (implicitly) included and the coroots are included for root systems. Empirically this seems to be by far the most convenient design and by providing extensionality lemmas expressing the uniqueness we expect to get the best of both worlds.

A final point is that we require roots and coroots to be injections from a base indexing type ι rather than subsets of their codomains. This design was chosen to avoid the bijection between roots and coroots being a dependently-typed object. A third option would be to have the roots and coroots be subsets but to avoid having a dependently-typed bijection by defining it globally with junk value 0 outside of the roots and coroots. This would work but lacks the convenient symmetry that the chosen design enjoys: by introducing the indexing type ι, one does not have to pick a direction (roots → coroots or coroots → roots) for the forward direction of the bijection. Besides, providing the user with the additional definitional power to specify an indexing type ι is a benefit and the junk-value pattern is a cost.