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.IsAnisotropic: We say a finite root pairing is anisotropic if there are no roots / coroots which have length zero wrt the root / coroot forms.
• 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.
• RootPairing.rootForm_restrict_nondegenerate_of_ordered: The root form is non-degenerate if the coefficients are ordered.
• RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic: the root form is non-degenerate if the coefficients are a field and the pairing is crystallographic.

References:

• N. Bourbaki, Lie groups and Lie algebras. Chapters 4--6
• M. Demazure, SGA III, Exposé XXI, Donné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.

class RootPairing.IsAnisotropic {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) : Prop

We say a finite root pairing is anisotropic if there are no roots / coroots which have length zero wrt the root / coroot forms.

Examples include crystallographic pairings in characteristic zero RootPairing.instIsAnisotropicOfIsCrystallographic and pairings over ordered scalars. RootPairing.instIsAnisotropicOfLinearOrderedCommRing.

• rootForm_root_ne_zero (i : ι) : (P.RootForm (P.root i)) (P.root i) ≠ 0
• corootForm_coroot_ne_zero (i : ι) : (P.CorootForm (P.coroot i)) (P.coroot i) ≠ 0

instance RootPairing.instIsAnisotropicFlip {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : P.flip.IsAnisotropic

theorem RootPairing.isAnisotropic_of_isValuedIn {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) (S : Type u_5) [LinearOrderedCommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] : P.IsAnisotropic

instance RootPairing.instIsAnisotropicOfIsCrystallographic {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) [CharZero R] [P.IsCrystallographic] : P.IsAnisotropic

@[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 ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [IsDomain R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : 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 ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [IsDomain R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : Module.finrank R ↥P.corootSpan = Module.finrank R ↥P.rootSpan

theorem RootPairing.disjoint_rootSpan_ker_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [IsDomain R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : Disjoint P.rootSpan (LinearMap.ker P.RootForm)

theorem RootPairing.disjoint_corootSpan_ker_corootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [CommRing R] [IsDomain R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : Disjoint P.corootSpan (LinearMap.ker P.CorootForm)

theorem RootPairing.isCompl_rootSpan_ker_rootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : IsCompl P.rootSpan (LinearMap.ker P.RootForm)

theorem RootPairing.isCompl_corootSpan_ker_corootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : IsCompl P.corootSpan (LinearMap.ker P.CorootForm)

theorem RootPairing.ker_rootForm_eq_dualAnnihilator {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : LinearMap.ker P.RootForm = Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator

theorem RootPairing.ker_corootForm_eq_dualAnnihilator {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : LinearMap.ker P.CorootForm = Submodule.map P.toDualRight.symm P.rootSpan.dualAnnihilator

instance RootPairing.instIsBalanced_1 {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : P.IsBalanced

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

See also RootPairing.rootForm_restrict_nondegenerate_of_ordered.

Note that this applies to crystallographic root systems in characteristic zero via RootPairing.instIsAnisotropicOfIsCrystallographic.

@[simp]

theorem RootPairing.orthogonal_rootSpan_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : P.RootForm.orthogonal P.rootSpan = LinearMap.ker P.RootForm

@[simp]

theorem RootPairing.orthogonal_corootSpan_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : P.CorootForm.orthogonal P.corootSpan = LinearMap.ker P.CorootForm

theorem RootPairing.rootSpan_eq_top_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [AddCommGroup M] [AddCommGroup N] [Field R] [Module R M] [Module R N] (P : RootPairing ι R M N) [P.IsAnisotropic] : P.rootSpan = ⊤ ↔ P.corootSpan = ⊤

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

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

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

See also RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic.

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

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 ι] [AddCommGroup M] [AddCommGroup N] [LinearOrderedCommRing R] [Module R M] [Module R N] (P : RootPairing ι R M N) {x : M} (hx : x ∈ P.rootSpan) (hx' : (P.RootForm x) x = 0) : x = 0

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

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