Upper-unitriangular positive Kostant subsystem groups

Let a Kostant form act on an integral lattice with a finite ordered weight basis. Suppose that a set S of distinguished root vectors acts by positive weight shifts: whenever a positive divided power carries the weight at basis index s to the weight at r, one has r < s. The individual root-subgroup matrices are then upper unitriangular by TauCeti.UniversalEnvelopingAlgebra.isUpperUnitriangular_kostantRootSubgroupMatrix.

This file passes from those individual root subgroups to the subgroup they generate. In basis coordinates the whole subsystem group lies in the upper-unitriangular group, giving a faithful homomorphism into that group. In particular the subsystem group is nilpotent, with no separate root-string or commutator hypotheses. The basis is indexed by an arbitrary finite linearly ordered type, which specializes to the Fin n carrier of the represented GLₙ scheme downstream.

For a Chevalley system and S the positive roots, this is the group-level bridge from the positive root-subgroup maps to the unipotent radical candidate in the Borel datum of the pinned Chevalley--Demazure group scheme.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.map_kostantSubsystemSubgroup_le_upperUnitriangular: in ordered weight-basis coordinates, the subsystem group is upper unitriangular.
• TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemUpperUnitriangular: the resulting faithful homomorphism into the upper-unitriangular group.
• TauCeti.UniversalEnvelopingAlgebra.isNilpotent_kostantSubsystemSubgroup_of_isPositive: a subsystem generated by positive weight shifts is nilpotent.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§21, 26--27.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 8.2.

This advances the pinning target of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Its positive-root subgroup is consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md in the construction of the Borel and ambient pinned group underlying TauCeti.ValidLieTypeIndex.AmbientGroup.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantSubsystemSubgroup_le_upperUnitriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type x} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (α : ι → κ → ℤ) (S : Set ι) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : η} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) (A : Type v) [CommRing A] : Subgroup.map (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv) (kostantSubsystemSubgroup e h ρ M hM hnil S ↧A) ≤ upperUnitriangularGroup η A

A subsystem generated by positive weight shifts is upper unitriangular in ordered weight-basis coordinates.

The conclusion concerns the entire subgroup generated by the selected root subgroups, not only its generators. Closure is supplied by the upper-unitriangular subgroup itself.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemUpperUnitriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type x} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (α : ι → κ → ℤ) (S : Set ι) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : η} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) (A : Type v) [CommRing A] : ↥(kostantSubsystemSubgroup e h ρ M hM hnil S ↧A) →* ↥(upperUnitriangularGroup η A)

The faithful homomorphism from a positive Kostant subsystem group to the upper-unitriangular group, obtained by writing its action in the ordered weight basis.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantSubsystemUpperUnitriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type x} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (α : ι → κ → ℤ) (S : Set ι) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : η} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) (A : Type v) [CommRing A] (g : ↥(kostantSubsystemSubgroup e h ρ M hM hnil S ↧A)) : ↑((kostantSubsystemUpperUnitriangular e h ρ M hM hnil b wt α S hwt hα hpos A) g) = (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv) ↑g

Forgetting the upper-unitriangular codomain recovers the matrix of the subsystem element in the ordered weight basis.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantSubsystemUpperUnitriangular_injective {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type x} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (α : ι → κ → ℤ) (S : Set ι) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : η} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) (A : Type v) [CommRing A] : Function.Injective ⇑(kostantSubsystemUpperUnitriangular e h ρ M hM hnil b wt α S hwt hα hpos A)

The upper-unitriangular representation of a positive Kostant subsystem group is injective.

theorem TauCeti.UniversalEnvelopingAlgebra.isNilpotent_kostantSubsystemSubgroup_of_isPositive {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type x} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [LinearOrder η] (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (α : ι → κ → ℤ) (S : Set ι) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : η} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) [Finite η] (A : Type v) [CommRing A] : Group.IsNilpotent ↥(kostantSubsystemSubgroup e h ρ M hM hnil S ↧A)

A Kostant subsystem generated by positive weight shifts is nilpotent. It embeds faithfully in the nilpotent upper-unitriangular group in ordered weight-basis coordinates.