Root data and root systems #
This file contains basic results for root systems and root data.
Main definitions / results: #
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.RootPairing.mk': In characteristic zero if there is no torsion, to check that two finite families of roots and coroots form a root pairing, it is sufficient to check that they are stable under reflections.RootSystem.mk': In characteristic zero if there is no torsion, to check that a finite 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.
The bijection on the indexing set induced by reflection.
Equations
Instances For
Even though the roots may not span, coroots are distinguished by their pairing with the roots. The proof depends crucially on the fact that there are finitely-many roots.
Modulo trivial generalisations, this statement is exactly Lemma 1.1.4 on page 87 of SGA 3 XXI.
In characteristic zero if there is no torsion, the correspondence between roots and coroots is unique.
Formally, the point is that the hypothesis hc depends only on the range of the coroot mappings.
In characteristic zero if there is no torsion, to check that two finite families of roots and coroots form a root pairing, it is sufficient to check that they are stable under reflections.
Equations
Instances For
In characteristic zero if there is no torsion, a finite root system is determined entirely by its roots.
Alias of RootPairing.IsRootSystem.ext.
In characteristic zero if there is no torsion, a finite root system is determined entirely by its roots.
Over a field of characteristic zero, to check that a finite family of roots form a crystallographic 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. Likewise, we do not need to check that the coroots span.
Equations
Instances For
Alias of RootPairing.mk''.
Over a field of characteristic zero, to check that a finite family of roots form a crystallographic 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. Likewise, we do not need to check that the coroots span.