The canonical bilinear form on a finite root pairing

Given a finite root pairing, we define a canonical map from weight space to coweight space, and the corresponding bilinear form. This form is symmetric and Weyl-invariant, and if the base ring is linearly ordered, then the form is root-positive, positive-semidefinite on the weight space, 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 crystallographic root pairing are restricted to a small finite set of possibilities. Another application is to the faithfulness of the Weyl group action on roots, and finiteness of the Weyl group.

Main definitions:

• Polarization: A distinguished linear map from the weight space to the coweight space.
• RootForm : The bilinear form on weight space corresponding to Polarization.

Main results:

• polarization_self_sum_of_squares : The inner product of any weight vector is a sum of squares.
• rootForm_reflection_reflection_apply : RootForm is invariant with respect to reflections.
• rootForm_self_smul_coroot: The inner product of a root with itself times the corresponding coroot is equal to two times Polarization applied to the root.
• rootForm_self_non_neg: RootForm is positive semidefinite.

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 (possibly in other files)

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

def RootPairing.Polarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : M →ₗ[R] N

An invariant linear map from weight space to coweight space.

Equations

• P.Polarization = ∑ i : ι, LinearMap.toSpanSingleton R N (P.coroot i) ∘ₗ P.coroot' i

@[simp]

theorem RootPairing.Polarization_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x : M) : P.Polarization x = ∑ i : ι, (P.coroot' i) x • P.coroot i

def RootPairing.CoPolarization {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : N →ₗ[R] M

An invariant linear map from coweight space to weight space.

Equations

• P.CoPolarization = ∑ i : ι, LinearMap.toSpanSingleton R M (P.root i) ∘ₗ P.root' i

@[simp]

theorem RootPairing.CoPolarization_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x : N) : P.CoPolarization x = ∑ i : ι, (P.root' i) x • P.root i

theorem RootPairing.CoPolarization_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : P.CoPolarization = P.flip.Polarization

def RootPairing.RootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : LinearMap.BilinForm R M

An invariant inner product on the weight space.

Equations

• P.RootForm = ∑ i : ι, LinearMap.smulRight (P.coroot' i) (P.coroot' i)

def RootPairing.CorootForm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : LinearMap.BilinForm R N

An invariant inner product on the coweight space.

Equations

• P.CorootForm = ∑ i : ι, LinearMap.smulRight (P.root' i) (P.root' i)

theorem RootPairing.rootForm_apply_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x y : M) : (P.RootForm x) y = ∑ i : ι, (P.coroot' i) x * (P.coroot' i) y

theorem RootPairing.rootForm_symmetric {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : LinearMap.IsSymm P.RootForm

@[simp]

theorem RootPairing.rootForm_reflection_reflection_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) (x y : M) : (P.RootForm ((P.reflection i) x)) ((P.reflection i) y) = (P.RootForm x) y

theorem RootPairing.rootForm_self_smul_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) : (P.RootForm (P.root i)) (P.root i) • P.coroot i = 2 • P.Polarization (P.root i)

This is SGA3 XXI Lemma 1.2.1 (10), key for proving nondegeneracy and positivity.

theorem RootPairing.corootForm_self_smul_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (i : ι) : (P.CorootForm (P.coroot i)) (P.coroot i) • P.root i = 2 • P.CoPolarization (P.coroot i)

theorem RootPairing.rootForm_self_sum_of_squares {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (x : M) : IsSumSq ((P.RootForm x) x)

theorem RootPairing.rootForm_root_self {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (j : ι) : (P.RootForm (P.root j)) (P.root j) = ∑ i : ι, P.pairing j i * P.pairing j i

theorem RootPairing.range_polarization_domRestrict_le_span_coroot {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Fintype ι] [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : LinearMap.range (P.Polarization.domRestrict P.rootSpan) ≤ P.corootSpan

theorem RootPairing.rootForm_self_non_neg {ι : 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) : 0 ≤ (P.RootForm x) x

theorem RootPairing.rootForm_self_zero_iff {ι : 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) : (P.RootForm x) x = 0 ↔ ∀ (i : ι), (P.coroot' i) x = 0

theorem RootPairing.rootForm_root_self_pos {ι : 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) (j : ι) : 0 < (P.RootForm (P.root j)) (P.root j)

theorem RootPairing.prod_rootForm_root_self_pos {ι : 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) : 0 < ∏ i : ι, (P.RootForm (P.root i)) (P.root i)

theorem RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict {ι : 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) (i : ι) : (∏ a : ι, (P.RootForm (P.root a)) (P.root a)) • P.coroot i ∈ LinearMap.range (P.Polarization.domRestrict P.rootSpan)