Invariant and 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.InvariantForm: an invariant bilinear form on a root pairing.
• 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_eq_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.

structure RootPairing.InvariantForm {ι : 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) : Type (max u_2 u_4)

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

• form : LinearMap.BilinForm R M

  The bilinear form bundled inside an InvariantForm.

• symm : LinearMap.IsSymm self.form
• ne_zero (i : ι) : (self.form (P.root i)) (P.root i) ≠ 0
• isOrthogonal_reflection (i : ι) : LinearMap.IsOrthogonal self.form ⇑(P.reflection i)

theorem RootPairing.InvariantForm.apply_root_ne_zero {ι : 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 : P.InvariantForm) (i : ι) : B.form (P.root i) ≠ 0

theorem RootPairing.InvariantForm.two_mul_apply_root_root {ι : 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 : P.InvariantForm) (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.InvariantForm.pairing_mul_eq_pairing_mul_swap {ι : 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 : P.InvariantForm) (i j : ι) : P.pairing j i * (B.form (P.root i)) (P.root i) = P.pairing i j * (B.form (P.root j)) (P.root j)

@[simp]

theorem RootPairing.InvariantForm.apply_reflection_reflection {ι : 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 : P.InvariantForm) (i : ι) (x y : M) : (B.form ((P.reflection i) x)) ((P.reflection i) y) = (B.form x) y

@[simp]

theorem RootPairing.InvariantForm.apply_weylGroup_smul {ι : 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 : P.InvariantForm) (g : ↥P.weylGroup) (x y : M) : (B.form (g • x)) (g • y) = (B.form x) y

@[simp]

theorem RootPairing.InvariantForm.apply_root_root_zero_iff {ι : 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 : P.InvariantForm) (i j : ι) [IsDomain R] [NeZero 2] : (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0

structure RootPairing.RootPositiveForm {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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.form_apply_root_ne_zero {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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.toInvariantForm {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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] : P.InvariantForm

Forgetting the positivity condition, we may regard a RootPositiveForm as an InvariantForm.

Equations

• B.toInvariantForm = { form := B.form, symm := ⋯, ne_zero := ⋯, isOrthogonal_reflection := ⋯ }

@[simp]

theorem RootPairing.RootPositiveForm.toInvariantForm_form {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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] : B.toInvariantForm.form = B.form

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} [CommRing S] [LinearOrder 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] : 2 * (B.form (P.root i)) (P.root j) = P.pairing i j * (B.form (P.root j)) (P.root j)

def RootPairing.RootPositiveForm.posForm {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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} [CommRing S] [LinearOrder 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} [CommRing S] [LinearOrder 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} [CommRing S] [LinearOrder 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} [CommRing S] [LinearOrder 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} [CommRing S] [LinearOrder 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

def RootPairing.RootPositiveForm.rootLength {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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 : ι) : S

The length of the i-th root wrt a root-positive form taking values in S.

Equations

• B.rootLength i = (B.posForm (P.rootSpanMem S i)) (P.rootSpanMem S i)

theorem RootPairing.RootPositiveForm.rootLength_pos {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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 : ι) : 0 < B.rootLength i

@[simp]

theorem RootPairing.RootPositiveForm.rootLength_reflectionPerm_self {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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 : ι) : B.rootLength ((P.reflectionPerm i) i) = B.rootLength i

@[deprecated RootPairing.RootPositiveForm.rootLength_reflectionPerm_self (since := "2025-05-28")]

theorem RootPairing.RootPositiveForm.rootLength_reflection_perm_self {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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 : ι) : B.rootLength ((P.reflectionPerm i) i) = B.rootLength i

Alias of RootPairing.RootPositiveForm.rootLength_reflectionPerm_self.

@[simp]

theorem RootPairing.RootPositiveForm.algebraMap_rootLength {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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 : ι) : (algebraMap S R) (B.rootLength i) = (B.form (P.root i)) (P.root i)

theorem RootPairing.RootPositiveForm.pairingIn_mul_eq_pairingIn_mul_swap {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing S] [LinearOrder 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] : P.pairingIn S j i * B.rootLength i = P.pairingIn S i j * B.rootLength j

@[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} [CommRing S] [LinearOrder 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] [IsStrictOrderedRing S] (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} [CommRing S] [LinearOrder 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] [IsStrictOrderedRing S] : 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} [CommRing S] [LinearOrder 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] [IsStrictOrderedRing S] : 0 ≤ P.coxeterWeightIn S i j