The Kostant torus--elementary subgroup as a semidirect product

Let U_S(A) be the subgroup generated by the represented Kostant root subgroups indexed by a set S of roots over a commutative value ring A, and let T(A) be the image of the diagonal action of the split weight torus. Their join B_S(A) = U_S(A) ⊔ T(A) is TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup, built in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Borel, where it is also shown that T(A) normalizes U_S(A) by the pinning equation t(s) xᵢ(u) t(s)⁻¹ = xᵢ(α(s) u).

This file packages that normalization as an action of T(A) on U_S(A) and identifies B_S(A) with the image of the multiplication map out of the external semidirect product

U_S(A) ⋊ T(A) ⟶ B_S(A).

No injectivity is asserted: the represented torus can meet the root-generated subgroup, so identifying the join with an external semidirect product on the nose would need an additional disjointness hypothesis. The surjection nevertheless gives the normal form g = x * t for every element of B_S(A). Taking S = Set.univ, where U_S(A) is the full elementary subgroup by kostantSubsystemSubgroup_univ, this is the pointwise assembly step toward the pinned Chevalley--Demazure group scheme; representability of the assembled functor and the Borel and maximal-torus properties remain later parts of Layer 9 of the reductive-groups roadmap.

The two group-theoretic ingredients — the range of the semidirect-product multiplication map and the resulting membership normal form — are proved for an arbitrary normalizing pair of subgroups in TauCeti.GroupTheory.SemidirectProduct and are instantiated here.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemAction is the conjugation action of the torus on the root-generated subgroup, and TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMonoidHom is multiplication from the resulting external semidirect product.

Main results

• TauCeti.UniversalEnvelopingAlgebra.range_kostantTorusPoints_le_normalizer records the pinning equation as normalization by the whole torus subgroup.
• TauCeti.UniversalEnvelopingAlgebra.range_kostantTorusSubsystemMonoidHom proves that the multiplication map is onto B_S(A).
• TauCeti.UniversalEnvelopingAlgebra.mem_kostantTorusSubsystemSubgroup_iff gives the resulting x * t normal form.

References

• R. W. Carter, Simple Groups of Lie Type, Sections 4.4 and 7.1.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

The torus subgroup normalizes the root-generated subgroup

theorem TauCeti.UniversalEnvelopingAlgebra.range_kostantTorusPoints_le_normalizer {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [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_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) : kostantTorusSubgroup M b wt ↑A ≤ Subgroup.normalizer ↑(kostantSubsystemSubgroup e h ρ M hM hnil S A)

The represented split torus normalizes the subgroup generated by the root subgroups indexed by S. This is the subgroup form of the pointwise statement kostantTorusPoints_mem_normalizer_kostantSubsystemSubgroup.

The semidirect-product multiplication map

@[reducible, inline]

noncomputable abbrev TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemAction {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [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_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) : ↥(kostantTorusSubgroup M b wt ↑A) →* MulAut ↥(kostantSubsystemSubgroup e h ρ M hM hnil S A)

The action of the represented torus subgroup on the root-generated subgroup by conjugation.

Equations

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

@[reducible, inline]

abbrev TauCeti.UniversalEnvelopingAlgebra.KostantTorusSubsystemSemidirectProduct {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [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_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) : Type (max v w)

The external semidirect product attached to the conjugation action of the represented torus on the root-generated subgroup. Its multiplication map need not be injective.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMonoidHom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [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_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) : KostantTorusSubsystemSemidirectProduct e h ρ M hM hnil b wt hwt α S hα A →* LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M)

Multiplication from the torus action's external semidirect product to the ambient general linear group.

This is a reducible wrapper for SemidirectProduct.monoidHomSubgroup, so Mathlib's SemidirectProduct.monoidHomSubgroup_apply computes it as x.left * x.right without unfolding anything by hand; likewise Subgroup.normalizerMonoidHom_apply_apply_coe computes kostantTorusSubsystemAction as conjugation.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMonoidHom e h ρ M hM hnil b wt hwt α S hα A = SemidirectProduct.monoidHomSubgroup ⋯

theorem TauCeti.UniversalEnvelopingAlgebra.range_kostantTorusSubsystemMonoidHom {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [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_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) : (kostantTorusSubsystemMonoidHom e h ρ M hM hnil b wt hwt α S hα A).range = kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A

The range of the semidirect-product multiplication map is exactly the subgroup generated by the root subgroups indexed by S together with the represented torus.

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantTorusSubsystemSubgroup_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v} [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_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (α : ι → κ → ℤ) (S : Set ι) (hα : ∀ i ∈ S, ∀ (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (A : CommAlgCat ℤ) (g : LinearMap.GeneralLinearGroup (↑A) (TensorProduct ℤ ↑A ↥M)) : g ∈ kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S A ↔ ∃ x ∈ kostantSubsystemSubgroup e h ρ M hM hnil S A, ∃ t ∈ kostantTorusSubgroup M b wt ↑A, g = x * t

An element belongs to B_S(A) exactly when it is a product of an element of the root-generated subgroup U_S(A) followed by a represented torus point.