Documentation

Mathlib.LinearAlgebra.RootSystem.RootPositive

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: #

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.

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.

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] :

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

Equations
@[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] :
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] :

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
@[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] :
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
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 : ι) :
@[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 : ι) :
@[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 : ι) :

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] :