Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.Weight.Order

Ordering a Kostant weight basis #

The positive-root triangularity results for Kostant root subgroups require an integral weight basis ordered so that adding a positive multiple of a root moves to a smaller index. This file constructs such an ordering from a degree functional which is positive on the chosen roots.

For a finite weight-basis index η, orderedWeightIndexEquiv degree wt numbers the indices by Fin (Fintype.card η). It first orders indices by decreasing value of degree (wt x) and uses an arbitrary finite numbering only to break ties. Thus the mathematical property of the numbering does not depend on the tie-breaker: orderedWeight_lt_of_eq_add_nsmul proves that every positive weight shift moves strictly towards the beginning.

The final results apply this construction to the existing triangularity API. In particular, range_kostantRootSubgroupMatrix_le_upperUnitriangular_orderedWeightBasis places each root subgroup whose root has positive degree in the upper-unitriangular group without retaining an ordering hypothesis.

Main definitions #

Main results #

References #

This supplies the ordered positive-root basis needed by the Borel component of the pinned Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which is consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

Ordering finite weight indices #

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.orderedWeightIndexEquiv {κ : Type u_1} {η : Type u_2} {D : Type u_3} [AddCommGroup D] [LinearOrder D] [Fintype η] (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) :
η ≃ Fin (Fintype.card η)

Number a finite family of weights by decreasing value under degree. Indices of equal degree are ordered by an arbitrary finite numbering; no theorem below depends on that tie-breaker.

Equations
Instances For
    source
    theorem TauCeti.UniversalEnvelopingAlgebra.orderedWeightIndexEquiv_lt_of_degree_lt {κ : Type u_1} {η : Type u_2} {D : Type u_3} [AddCommGroup D] [LinearOrder D] [Fintype η] (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) {r s : η} (hrs : degree (wt s) < degree (wt r)) :
    (orderedWeightIndexEquiv degree wt) r < (orderedWeightIndexEquiv degree wt) s

    A strictly larger weight degree receives a strictly smaller ordered index.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.orderedWeightIndexEquiv_lt_of_eq_add_nsmul {κ : Type u_1} {η : Type u_2} {D : Type u_3} [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D] [Fintype η] (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) {α : κ → ℤ} (hα : 0 < degree α) {r s : η} {n : ℕ} (hn : 0 < n) (hrs : wt r = wt s + n • α) :
    (orderedWeightIndexEquiv degree wt) r < (orderedWeightIndexEquiv degree wt) s

    Adding a positive multiple of a positive-degree root strictly decreases the ordered index.

    The ordered basis and its weights #

    source
    noncomputable def TauCeti.UniversalEnvelopingAlgebra.orderedWeightBasis {κ : Type u_1} {η : Type u_2} {V : Type v} [AddCommGroup V] {D : Type u_3} [AddCommGroup D] [LinearOrder D] [Fintype η] (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) (b : Module.Basis η ℤ V) :
    Module.Basis (Fin (Fintype.card η)) ℤ V

    A finite basis reindexed by decreasing degree of its recorded weights.

    Equations
    Instances For
      source
      noncomputable def TauCeti.UniversalEnvelopingAlgebra.orderedWeight {κ : Type u_1} {η : Type u_2} {D : Type u_3} [AddCommGroup D] [LinearOrder D] [Fintype η] (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) :
      Fin (Fintype.card η) → κ → ℤ

      The weight attached to an index of orderedWeightBasis.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.UniversalEnvelopingAlgebra.orderedWeightBasis_apply {κ : Type u_1} {η : Type u_2} {V : Type v} [AddCommGroup V] {D : Type u_3} [AddCommGroup D] [LinearOrder D] [Fintype η] (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) (b : Module.Basis η ℤ V) (x : Fin (Fintype.card η)) :
        (orderedWeightBasis degree wt b) x = b ((orderedWeightIndexEquiv degree wt).symm x)
        source
        @[simp]
        theorem TauCeti.UniversalEnvelopingAlgebra.orderedWeight_apply {κ : Type u_1} {η : Type u_2} {D : Type u_3} [AddCommGroup D] [LinearOrder D] [Fintype η] (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) (x : Fin (Fintype.card η)) :
        orderedWeight degree wt x = wt ((orderedWeightIndexEquiv degree wt).symm x)
        source
        theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_orderedWeightBasis {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {η : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {D : Type u_3} [AddCommGroup D] [LinearOrder D] [Fintype η] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) (b : Module.Basis η ℤ V) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) (b x)) (x : Fin (Fintype.card η)) :
        IsCartanWeightVector h ρ (orderedWeight degree wt x) ((orderedWeightBasis degree wt b) x)

        The ordered basis has the same weight-vector property as the original basis.

        source
        theorem TauCeti.UniversalEnvelopingAlgebra.orderedWeight_lt_of_eq_add_nsmul {κ : Type u_1} {η : Type u_2} {D : Type u_3} [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D] [Fintype η] (degree : (κ → ℤ) →+ D) (wt : η → κ → ℤ) {α : κ → ℤ} (hα : 0 < degree α) {r s : Fin (Fintype.card η)} {n : ℕ} (hn : 0 < n) (hrs : orderedWeight degree wt r = orderedWeight degree wt s + n • α) :
        r < s

        In the reindexed weight basis, adding a positive multiple of a positive-degree root moves strictly towards the beginning. This is the order hypothesis used by positive-root triangularity.

        Positive root subgroups in the ordered basis #

        source
        theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_coe_orderedWeightBasis {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {η : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {D : Type u_3} [AddCommGroup D] [LinearOrder D] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) [Fintype η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (degree : (κ → ℤ) →+ D) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (x : Fin (Fintype.card η)) :
        IsCartanWeightVector h ρ (orderedWeight degree wt x) ↑((orderedWeightBasis degree wt b) x)

        Reindexing a subgroup basis preserves its weight-vector property after coercion to the ambient rational representation.

        source
        theorem TauCeti.UniversalEnvelopingAlgebra.isUpperTriangular_toMatrix_integralDividedPower_orderedWeightBasis {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {η : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {D : Type u_3} [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) [Fintype η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (degree : (κ → ℤ) →+ D) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) {i : ι} {α : κ → ℤ} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (hdegree : 0 < degree α) {n : ℕ} (hn : 0 < n) :
        ((LinearMap.toMatrix (orderedWeightBasis degree wt b) (orderedWeightBasis degree wt b)) (integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M n ⋯)).IsUpperTriangular

        A root operator of positive degree is strictly upper triangular in every positive divided power when the underlying weight basis is reordered by decreasing degree.

        source
        theorem TauCeti.UniversalEnvelopingAlgebra.isUpperUnitriangular_kostantRootSubgroupMatrix_orderedWeightBasis {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {η : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {D : Type u_3} [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) [Fintype η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (degree : (κ → ℤ) →+ D) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) {i : ι} {α : κ → ℤ} (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (hdegree : 0 < degree α) {A : Type u_4} [CommRing A] (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) :
        (↑((kostantRootSubgroupMatrix e h ρ M hM i hnil (orderedWeightBasis degree wt b)) f)).IsUpperUnitriangular

        A root subgroup of positive degree is upper unitriangular in the weight basis ordered by decreasing degree. The choice used to order equal-degree weight spaces does not enter the proof.

        source
        theorem TauCeti.UniversalEnvelopingAlgebra.range_kostantRootSubgroupMatrix_le_upperUnitriangular_orderedWeightBasis {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {η : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {D : Type u_3} [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) [Fintype η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (degree : (κ → ℤ) →+ D) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) {i : ι} {α : κ → ℤ} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (hdegree : 0 < degree α) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {A : Type u_4} [CommRing A] :
        (kostantRootSubgroupMatrix e h ρ M hM i hnil (orderedWeightBasis degree wt b)).range ≤ upperUnitriangularGroup (Fin (Fintype.card η)) A

        The image of every positive-degree root subgroup lies in the upper-unitriangular subgroup after reindexing the weight basis by decreasing degree.