Nondegeneracy of the polarization on a finite root pairing

We show that if the base ring of a finite root pairing is linearly ordered, then the canonical bilinear form is root-positive and positive-definite on the span of roots. From these facts, it is easy to show that Coxeter weights in a finite root pairing are bounded above by 4. Thus, the pairings of roots and coroots in a root pairing are restricted to the interval [-4, 4]. Furthermore, a linearly independent pair of roots cannot have Coxeter weight 4. For the case of crystallographic root pairings, we are thus reduced to a finite set of possible options for each pair. Another application is to the faithfulness of the Weyl group action on roots, and finiteness of the Weyl group.

Main results:

• RootPairing.rootForm_rootPositive: RootForm is root-positive.
• RootPairing.polarization_domRestrict_injective: The polarization restricted to the span of roots is injective.
• RootPairing.rootForm_pos_of_nonzero: RootForm is strictly positive on non-zero linear combinations of roots. This gives us a convenient way to eliminate certain Dynkin diagrams from the classification, since it suffices to produce a nonzero linear combination of simple roots with non-positive norm.

References:

• N. Bourbaki, Lie groups and {L}ie algebras. {C}hapters 4--6
• M. Demazure, SGA III, Expos'{e} XXI, Don'{e}es Radicielles

Todo

• Weyl-invariance of RootForm and CorootForm
• Faithfulness of Weyl group perm action, and finiteness of Weyl group, over ordered rings.
• Relation to Coxeter weight. In particular, positivity constraints for finite root pairings mean we restrict to weights between 0 and 4.

theorem RootPairing.rootForm_rootPositive {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : P.IsRootPositive P.RootForm

instance RootPairing.instFiniteSubtypeMemSubmoduleRootSpan {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : Module.Finite R ↥P.rootSpan

Equations

• ⋯ = ⋯

instance RootPairing.instFiniteSubtypeMemSubmoduleCorootSpan {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : Module.Finite R ↥P.corootSpan

Equations

• ⋯ = ⋯

@[simp]

theorem RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : Module.finrank R ↥(Submodule.map P.Polarization P.rootSpan) = Module.finrank R ↥P.corootSpan

theorem RootPairing.finrank_corootSpan_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : Module.finrank R ↥P.corootSpan = Module.finrank R ↥P.rootSpan

theorem RootPairing.disjoint_rootSpan_ker_polarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : Disjoint P.rootSpan (LinearMap.ker P.Polarization)

theorem RootPairing.mem_ker_polarization_of_rootForm_self_eq_zero {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) {x : M} (hx : (P.RootForm x) x = 0) : x ∈ LinearMap.ker P.Polarization

theorem RootPairing.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) {x : M} (hx : x ∈ P.rootSpan) (hx' : (P.RootForm x) x = 0) : x = 0

theorem RootSystem.rootForm_anisotropic {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootSystem ι R M N) : (LinearMap.BilinMap.toQuadraticMap P.RootForm).Anisotropic

theorem RootPairing.rootForm_pos_of_nonzero {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) {x : M} (hx : x ∈ P.rootSpan) (h : x ≠ 0) : 0 < (P.RootForm x) x

theorem RootPairing.rootForm_restrict_nondegenerate {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : LinearMap.Nondegenerate (P.RootForm.restrict P.rootSpan)