Root-positive bilinear forms on root pairings

This file contains basic results on Weyl-invariant inner products for root systems and root data. Given a root pairing we define a structure which contains a bilinear form together with axioms for reflection-invariance, symmetry, and strict positivity on all roots. We show that root-positive forms display the same sign behavior as the canonical pairing between roots and coroots.

Root-positive forms show up naturally as the invariant forms for symmetrizable Kac-Moody Lie algebras. In the finite case, the canonical polarization yields a root-positive form that is positive semi-definite on weight space and positive-definite on the span of roots.

Main definitions / results:

• RootPairing.RootPositiveForm: Given a root pairing this is a structure which contains a bilinear form together with axioms for reflection-invariance, symmetry, and strict positivity on all roots.
• RootPairing.zero_lt_pairingIn_iff: sign relations between RootPairing.pairingIn and a root-positive form.
• RootPairing.pairing_zero_iff: symmetric vanishing condition for RootPairing.pairing
• RootPairing.coxeterWeight_nonneg: All pairs of roots have non-negative Coxeter weight.
• RootPairing.coxeterWeight_zero_iff_isOrthogonal : A Coxeter weight vanishes iff the roots are orthogonal.

TODO

• Invariance under the Weyl group.

theorem RootPairing.two_mul_apply_root_root_of_isOrthogonal {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (B : LinearMap.BilinForm R M) (i j : ι) (h : LinearMap.IsOrthogonal B ⇑(P.reflection j)) : 2 * (B (P.root i)) (P.root j) = P.pairing i j * (B (P.root j)) (P.root j)

structure RootPairing.RootPositiveForm {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [P.IsValuedIn S] : Type (max u_2 u_4)

Given a root pairing, this is an invariant symmetric bilinear form satisfying a positivity condition.

• form : LinearMap.BilinForm R M

  The bilinear form bundled inside a RootPositiveForm.

• symm : LinearMap.IsSymm self.form
• isOrthogonal_reflection (i : ι) : LinearMap.IsOrthogonal self.form ⇑(P.reflection i)
• exists_eq (i j : ι) : ∃ (s : S), (algebraMap S R) s = (self.form (P.root i)) (P.root j)
• exists_pos_eq (i : ι) : ∃ s > 0, (algebraMap S R) s = (self.form (P.root i)) (P.root i)

theorem RootPairing.RootPositiveForm.two_mul_apply_root_root {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) (i j : ι) : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * (B.form (P.root j)) (P.root j)

theorem RootPairing.RootPositiveForm.form_apply_root_ne_zero {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) [FaithfulSMul S R] (i : ι) : (B.form (P.root i)) (P.root i) ≠ 0

def RootPairing.RootPositiveForm.posForm {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] : LinearMap.BilinForm S ↥(Submodule.span S (Set.range ⇑P.root))

Given a root-positive form associated to a root pairing with coefficients in R but taking values in S, this is the associated S-bilinear form on the S-span of the roots.

Equations

• B.posForm = (Submodule.span S (Set.range ⇑P.root)).subtype.restrictScalarsRange (Submodule.span S (Set.range ⇑P.root)).subtype (Algebra.linearMap S R) ⋯ B.form ⋯

@[simp]

theorem RootPairing.RootPositiveForm.algebraMap_posForm {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] {x y : ↥(Submodule.span S (Set.range ⇑P.root))} : (algebraMap S R) ((B.posForm x) y) = (B.form ↑x) ↑y

theorem RootPairing.RootPositiveForm.algebraMap_apply_eq_form_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] {x y : ↥(Submodule.span S (Set.range ⇑P.root))} {s : S} : (algebraMap S R) s = (B.form ↑x) ↑y ↔ s = (B.posForm x) y

theorem RootPairing.RootPositiveForm.zero_lt_posForm_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] {x y : ↥(Submodule.span S (Set.range ⇑P.root))} : 0 < (B.posForm x) y ↔ ∃ s > 0, (algebraMap S R) s = (B.form ↑x) ↑y

theorem RootPairing.RootPositiveForm.zero_lt_posForm_apply_root {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] (i : ι) (hi : P.root i ∈ Submodule.span S (Set.range ⇑P.root) := ⋯) : 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root i, hi⟩

theorem RootPairing.RootPositiveForm.isSymm_posForm {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] : LinearMap.IsSymm B.posForm

@[simp]

theorem RootPairing.RootPositiveForm.zero_lt_apply_root_root_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) (i j : ι) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] (hi : P.root i ∈ Submodule.span S (Set.range ⇑P.root) := ⋯) (hj : P.root j ∈ Submodule.span S (Set.range ⇑P.root) := ⋯) : 0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ↔ 0 < P.pairingIn S i j

theorem RootPairing.zero_lt_pairingIn_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) (i j : ι) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] : 0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i

theorem RootPairing.coxeterWeight_nonneg {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) (i j : ι) [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] : 0 ≤ P.coxeterWeightIn S i j

@[simp]

theorem RootPairing.apply_root_root_zero_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) (i j : ι) [FaithfulSMul S R] [NoZeroDivisors R] : (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0

theorem RootPairing.pairing_zero_iff {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) (i j : ι) [FaithfulSMul S R] [NoZeroDivisors R] : P.pairing i j = 0 ↔ P.pairing j i = 0

theorem RootPairing.coxeterWeight_zero_iff_isOrthogonal {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [LinearOrderedCommRing S] [CommRing R] [Algebra S R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) (i j : ι) [FaithfulSMul S R] [NoZeroDivisors R] : P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j