Positive Kostant subsystem schemes are upper triangular

Let a Kostant form act on an integral lattice with a finite ordered weight basis. If the selected root operators raise weights strictly towards the beginning of that basis, their represented root subgroups are upper unitriangular, while the represented weight torus is diagonal. Consequently, the closed subgroup scheme generated by the selected root subgroups and the weight torus is contained in the standard upper-triangular subgroup scheme.

This is a scheme-theoretic statement: the upper-triangular defining Hopf ideal is contained in the common-kernel ideal defining the subsystem carrier. It gives an injective homomorphism from every algebra-valued point group of the subsystem into the solvable upper-triangular point group, so all of those point groups are solvable. For a positive system this supplies the solvability part of the Borel construction. Smoothness, connectedness, and maximality are separate geometric inputs.

Main results

• TauCeti.UniversalEnvelopingAlgebra. generalLinearUpperTriangularDefiningHopfIdeal_le_kostantTorusSubsystemDefiningIdeal: the positive subsystem carrier is scheme-theoretically contained in the upper-triangular group.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemToUpperTriangular: the resulting closed immersion of group schemes.
• TauCeti.UniversalEnvelopingAlgebra.isSolvable_points_kostantTorusSubsystem: every algebra-valued point group of the positive subsystem carrier is solvable.

References

• J. E. Humphreys, Linear Algebraic Groups, Sections 26--28.
• R. W. Carter, Simple Groups of Lie Type, Sections 4.4 and 8.2.

theorem TauCeti.UniversalEnvelopingAlgebra.generalLinearUpperTriangularDefiningHopfIdeal_le_kostantTorusSubsystemDefiningIdeal {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (α : I → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : Fin n} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) : GeneralLinear.UpperTriangular.definingHopfIdeal ℤ n ≤ kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS

A torus-plus-positive-root Kostant subsystem is contained in the standard upper-triangular group scheme. In Hopf coordinates, the upper-triangular defining ideal is contained in the common-kernel ideal of the selected root subgroups and the weight torus.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemToUpperTriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (α : I → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : Fin n} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) : kostantTorusSubsystemGroupScheme e h ρ M hM b wt S hnilS ⟶ GeneralLinear.UpperTriangular.groupScheme ℤ n

The canonical closed immersion from a torus-plus-positive-root Kostant subsystem into the standard upper-triangular group scheme.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemToUpperTriangular_def {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (α : I → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : Fin n} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) : kostantTorusSubsystemToUpperTriangular e h ρ M hM b wt α S hnilS hwt hα hpos = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecMapOfLe (GeneralLinear.coordinateHopfAlgebra ℤ n) ⋯) (CategoryTheory.eqToHom ⋯)

kostantTorusSubsystemToUpperTriangular is the quotient-spectrum map induced by containment of the upper-triangular defining Hopf ideal, followed by the canonical presentation isomorphism.

instance TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantTorusSubsystemToUpperTriangular {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (α : I → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : Fin n} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantTorusSubsystemToUpperTriangular e h ρ M hM b wt α S hnilS hwt hα hpos).hom.hom)

The positive subsystem map to the upper-triangular group scheme is a closed immersion.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemToUpperTriangular_comp_inclusion {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (α : I → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hpos : ∀ i ∈ S, ∀ {r s : Fin n} {m : ℕ}, 0 < m → wt r = wt s + m • α i → r < s) : CategoryTheory.CategoryStruct.comp (kostantTorusSubsystemToUpperTriangular e h ρ M hM b wt α S hnilS hwt hα hpos) (GeneralLinear.UpperTriangular.inclusion ℤ n) = kostantTorusSubsystemGroupSchemeι e h ρ M hM b wt S hnilS

The positive subsystem inclusion into GLₙ factors through the standard upper-triangular inclusion.

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

Every algebra-valued point group of a torus-plus-positive-root Kostant subsystem is solvable. The coordinate quotient from the upper-triangular group is surjective, so the contravariant map embeds subsystem points into upper-triangular points.