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

source
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.

Instances For
    source
    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
    source
    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)
    source
    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)
    source
    @[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
    source
    @[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
    source
    @[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 : ι) [NoZeroDivisors R] [NeZero 2] :
    (B.form (P.root i)) (P.root j) = 0 ↔ P.pairing i j = 0
    source
    theorem RootPairing.InvariantForm.pairing_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 : ι) [NoZeroDivisors R] [NeZero 2] :
    P.pairing i j = 0 ↔ P.pairing j i = 0
    source
    theorem RootPairing.InvariantForm.coxeterWeight_zero_iff_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 : P.InvariantForm) (i j : ι) [NoZeroDivisors R] [NeZero 2] :
    P.coxeterWeight i j = 0 ↔ P.IsOrthogonal i j
    source
    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.

    Instances For
      source
      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
      source
      def RootPairing.RootPositiveForm.toInvariantForm {ι : 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] :
      P.InvariantForm

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

      Equations
      Instances For
        source
        @[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} [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] :
        B.toInvariantForm.form = B.form
        source
        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 : ι) [FaithfulSMul S R] :
        2 * (B.form (P.root i)) (P.root j) = P.pairing i j * (B.form (P.root j)) (P.root j)
        source
        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
        Instances For
          source
          @[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
          source
          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
          source
          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
          source
          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⟩
          source
          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
          source
          @[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
          source
          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
          source
          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