Documentation

Mathlib.Algebra.Lie.Weights.Chain

Chains of roots and weights #

Given roots α and β of a Lie algebra, together with elements x in the α-root space and y in the β-root space, it follows from the Leibniz identity that ⁅x, y⁆ is either zero or belongs to the α + β-root space. Iterating this operation leads to the study of families of roots of the form k • α + β. Such a family is known as the α-chain through β (or sometimes, the α-string through β) and the study of the sum of the corresponding root spaces is an important technique.

More generally if α is a root and χ is a weight of a representation, it is useful to study the α-chain through χ.

We provide basic definitions and results to support α-chain techniques in this file.

Main definitions / results #

theorem LieModule.eventually_genWeightSpace_smul_add_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : LR) (χ₂ : LR) [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ 0) :
∀ᶠ (k : ) in Filter.atTop, LieModule.genWeightSpace M (k χ₁ + χ₂) =
theorem LieModule.exists_genWeightSpace_smul_add_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : LR) (χ₂ : LR) [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ 0) :
k > 0, LieModule.genWeightSpace M (k χ₁ + χ₂) =
theorem LieModule.exists₂_genWeightSpace_smul_add_eq_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : LR) (χ₂ : LR) [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hχ₁ : χ₁ 0) :
p < 0, q > 0, LieModule.genWeightSpace M (p χ₁ + χ₂) = LieModule.genWeightSpace M (q χ₁ + χ₂) =
def LieModule.genWeightSpaceChain {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : LR) (χ₂ : LR) (p : ) (q : ) :

Given two (potential) weights χ₁ and χ₂ together with integers p and q, it is often useful to study the sum of weight spaces associated to the family of weights k • χ₁ + χ₂ for p < k < q.

Equations
Instances For
    theorem LieModule.genWeightSpaceChain_def {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : LR) (χ₂ : LR) (p : ) (q : ) :
    LieModule.genWeightSpaceChain M χ₁ χ₂ p q = kSet.Ioo p q, LieModule.genWeightSpace M (k χ₁ + χ₂)
    theorem LieModule.genWeightSpaceChain_def' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : LR) (χ₂ : LR) (p : ) (q : ) :
    LieModule.genWeightSpaceChain M χ₁ χ₂ p q = kFinset.Ioo p q, LieModule.genWeightSpace M (k χ₁ + χ₂)
    @[simp]
    theorem LieModule.genWeightSpaceChain_neg {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : LR) (χ₂ : LR) (p : ) (q : ) :
    LieModule.genWeightSpaceChain M (-χ₁) χ₂ (-q) (-p) = LieModule.genWeightSpaceChain M χ₁ χ₂ p q
    theorem LieModule.genWeightSpace_le_genWeightSpaceChain {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] (χ₁ : LR) (χ₂ : LR) (p : ) (q : ) {k : } (hk : k Set.Ioo p q) :
    LieModule.genWeightSpace M (k χ₁ + χ₂) LieModule.genWeightSpaceChain M χ₁ χ₂ p q
    theorem LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (α : HR) (χ : HR) (p : ) (q : ) [LieAlgebra.IsNilpotent R H] (hq : LieModule.genWeightSpace M (q α + χ) = ) {x : L} (hx : x LieAlgebra.rootSpace H α) {y : M} (hy : y LieModule.genWeightSpaceChain M α χ p q) :
    theorem LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (α : HR) (χ : HR) (p : ) (q : ) [LieAlgebra.IsNilpotent R H] (hp : LieModule.genWeightSpace M (p α + χ) = ) {x : L} (hx : x LieAlgebra.rootSpace H (-α)) {y : M} (hy : y LieModule.genWeightSpaceChain M α χ p q) :
    theorem LieModule.trace_toEnd_genWeightSpaceChain_eq_zero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (α : HR) (χ : HR) (p : ) (q : ) [H.IsCartanSubalgebra] [IsNoetherian R L] (hp : LieModule.genWeightSpace M (p α + χ) = ) (hq : LieModule.genWeightSpace M (q α + χ) = ) {x : H} (hx : x LieAlgebra.corootSpace α) :
    theorem LieModule.exists_forall_mem_corootSpace_smul_add_eq_zero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {H : LieSubalgebra R L} (α : HR) (χ : HR) [H.IsCartanSubalgebra] [IsNoetherian R L] [IsDomain R] [IsPrincipalIdealRing R] [CharZero R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (hα : α 0) (hχ : LieModule.genWeightSpace M χ ) :
    ∃ (a : ) (b : ), 0 < b xLieAlgebra.corootSpace α, (a α + b χ) x = 0

    Given a (potential) root α relative to a Cartan subalgebra H, if we restrict to the ideal I = corootSpace α of H (informally, I = ⁅H(α), H(-α)⁆), we may find an integral linear combination between α and any weight χ of a representation.

    This is Proposition 4.4 from [Car05] and is a key step in the proof that the roots of a semisimple Lie algebra form a root system. It shows that the restriction of α to I vanishes iff the restriction of every root to I vanishes (which cannot happen in a semisimple Lie algebra).

    noncomputable def LieModule.chainTopCoeff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :

    This is the largest n : ℕ such that i • α + β is a weight for all 0 ≤ i ≤ n.

    Equations
    Instances For
      noncomputable def LieModule.chainBotCoeff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :

      This is the largest n : ℕ such that -i • α + β is a weight for all 0 ≤ i ≤ n.

      Equations
      Instances For
        @[simp]
        @[simp]
        theorem LieModule.chainTopCoeff_add_one {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) (hα : α 0) :
        theorem LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) (hα : α 0) :
        theorem LieModule.genWeightSpace_chainBotCoeff_sub_one_zsmul_sub {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) (hα : α 0) :
        theorem LieModule.genWeightSpace_zsmul_add_ne_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) {n : } (hn : -(LieModule.chainBotCoeff α β) n) (hn' : n (LieModule.chainTopCoeff α β)) :
        theorem LieModule.genWeightSpace_neg_zsmul_add_ne_bot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) {n : } (hn : n LieModule.chainBotCoeff α β) :
        noncomputable def LieModule.chainTop {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :

        The last weight in an α-chain through β.

        Equations
        Instances For
          noncomputable def LieModule.chainBot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :

          The first weight in an α-chain through β.

          Equations
          Instances For
            theorem LieModule.coe_chainTop' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :
            @[simp]
            theorem LieModule.coe_chainTop {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :
            (LieModule.chainTop α β) = (LieModule.chainTopCoeff α β) α + β
            @[simp]
            theorem LieModule.coe_chainBot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :
            (LieModule.chainBot α β) = -(LieModule.chainBotCoeff α β) α + β
            @[simp]
            theorem LieModule.chainTop_neg {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :
            @[simp]
            theorem LieModule.chainBot_neg {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) :
            @[simp]
            @[simp]
            theorem LieModule.genWeightSpace_add_chainTop {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) (hα : α 0) :
            theorem LieModule.genWeightSpace_neg_add_chainBot {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) (hα : α 0) :
            theorem LieModule.chainTop_isNonZero' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LR) (β : LieModule.Weight R L M) (hα : α 0) (hα' : LieModule.genWeightSpace M α ) :
            (LieModule.chainTop α β).IsNonZero
            theorem LieModule.chainTop_isNonZero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieAlgebra.IsNilpotent R L] [NoZeroSMulDivisors R] [NoZeroSMulDivisors R M] [IsNoetherian R M] (α : LieModule.Weight R L M) (β : LieModule.Weight R L M) (hα : α.IsNonZero) :
            (LieModule.chainTop (⇑α) β).IsNonZero