A symmetry criterion for reduced root pairings #
A finite root pairing over a characteristic-zero domain is reduced as soon as its pairing is
symmetric on roots and coroots. Indeed, two linearly dependent roots have Coxeter weight four.
Symmetry makes this weight the square of one pairing value, so that value is 2 or -2; the
root-pairing axioms then identify the two roots up to sign.
This criterion is useful for root data presented in dual coordinate bases. Their roots and coroots need not be equal as coordinate vectors, while the pairing can still visibly be the symmetric form of a simply-laced Cartan matrix.
Main result #
RootPairing.isReduced_of_pairing_comm: a finite root pairing with symmetric pairings is reduced.
theorem
RootPairing.isReduced_of_pairing_comm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CharZero R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[Module.IsTorsionFree R M]
[AddCommGroup N]
[Module R N]
(P : RootPairing ι R M N)
[Finite ι]
(hcomm : ∀ (i j : ι), P.pairing i j = P.pairing j i)
:
A finite root pairing whose root--coroot pairing is symmetric is reduced.