Root-positive bilinear forms on root pairings

This file contains basic results on Weyl-invariant inner products for root systems and root data. We introduce a Prop-valued mixin class for a root pairing and bilinear form, specifying 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:

• IsRootPositive: A prop-valued mixin class for root pairings with bilinear forms, specifying the form is symmetric, reflection-invariant, and all roots have strictly positive norm.

Main results:

• pairing_pos_iff and pairing_zero_iff : sign relations between P.pairing and the form B.
• coxeter_weight_non_neg : All pairs of roots have non-negative Coxeter weight.
• orthogonal_of_coxeter_weight_zero : If Coxeter weight vanishes, then the roots are orthogonal.

TODO

• Invariance under the Weyl group.

class RootPairing.IsRootPositive {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) (B : M →ₗ[R] M →ₗ[R] R) : Prop

A Prop-valued class for a bilinear form to be compatible with a root pairing.

• zero_lt_apply_root : ∀ (i : ι), 0 < (B (P.root i)) (P.root i)
• symm : ∀ (x y : M), (B x) y = (B y) x
• apply_reflection_eq : ∀ (i : ι) (x y : M), (B ((P.reflection i) x)) ((P.reflection i) y) = (B x) y

theorem RootPairing.IsRootPositive.zero_lt_apply_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} : ∀ {inst : LinearOrderedCommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} {B : M →ₗ[R] M →ₗ[R] R} [self : P.IsRootPositive B] (i : ι), 0 < (B (P.root i)) (P.root i)

theorem RootPairing.IsRootPositive.symm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} : ∀ {inst : LinearOrderedCommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} (P : RootPairing ι R M N) {B : M →ₗ[R] M →ₗ[R] R} [self : P.IsRootPositive B] (x y : M), (B x) y = (B y) x

theorem RootPairing.IsRootPositive.apply_reflection_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} : ∀ {inst : LinearOrderedCommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} {B : M →ₗ[R] M →ₗ[R] R} [self : P.IsRootPositive B] (i : ι) (x y : M), (B ((P.reflection i) x)) ((P.reflection i) y) = (B x) y

theorem RootPairing.two_mul_apply_root_root {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (B : M →ₗ[R] M →ₗ[R] R) [P.IsRootPositive B] (i : ι) (j : ι) : 2 * (B (P.root i)) (P.root j) = P.pairing i j * (B (P.root j)) (P.root j)

@[simp]

theorem RootPairing.zero_lt_apply_root_root_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (B : M →ₗ[R] M →ₗ[R] R) [P.IsRootPositive B] (i : ι) (j : ι) : 0 < (B (P.root i)) (P.root j) ↔ 0 < P.pairing i j

theorem RootPairing.zero_lt_pairing_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (B : M →ₗ[R] M →ₗ[R] R) [P.IsRootPositive B] (i : ι) (j : ι) : 0 < P.pairing i j ↔ 0 < P.pairing j i

theorem RootPairing.coxeterWeight_non_neg {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (B : M →ₗ[R] M →ₗ[R] R) [P.IsRootPositive B] (i : ι) (j : ι) : 0 ≤ P.coxeterWeight i j

@[simp]

theorem RootPairing.apply_root_root_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (B : M →ₗ[R] M →ₗ[R] R) [P.IsRootPositive B] (i : ι) (j : ι) : (B (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0

theorem RootPairing.pairing_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (B : M →ₗ[R] M →ₗ[R] R) [P.IsRootPositive B] (i : ι) (j : ι) : P.pairing i j = 0 ↔ P.pairing j i = 0

theorem RootPairing.coxeterWeight_zero_iff_isOrthogonal {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [LinearOrderedCommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} (B : M →ₗ[R] M →ₗ[R] R) [P.IsRootPositive B] (i : ι) (j : ι) : P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j