Matrix coordinates for Kostant root subgroups

Let M be a Kostant-stable integral lattice in a rational representation. A finite basis b : Basis η ℤ M gives every scalar extension A ⊗[ℤ] M the base-changed basis b.baseChange A. This file expresses the divided-power root subgroup action in that basis, as an invertible matrix over A indexed by η.

The resulting matrices are natural in the commutative value ring. They are the finite-coordinate input for the natural transformation whose representing morphism is the root subgroup 𝔾ₐ → GLₙ.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix: the matrix-valued root subgroup attached to a finite integral basis.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_apply: its entries are the coordinates of the divided-power exponential on basis vectors.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantRootSubgroupMatrix: matrix coordinates commute with maps of value rings.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• R. W. Carter, Simple Groups of Lie Type, §4.4.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {A : Type u_3} [CommRing A] : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A) →* GL η A

The Kostant root subgroup in matrix coordinates: the monoid homomorphism sending an A-point to the matrix of its action on A ⊗[ℤ] M in the base-changed basis b.baseChange A.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_def {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {A : Type u_3} [CommRing A] : kostantRootSubgroupMatrix e h ρ M hM i hnil b = (Units.map (LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv.toMonoidHom).comp (kostantRootSubgroupPoints e h ρ M hM i hnil)

The public unfolding equation for the matrix-valued root subgroup, exposing across the module boundary the divided-power action followed by the change to the coordinates of b.baseChange A.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {A : Type u_3} [CommRing A] (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (r s : η) : ↑((kostantRootSubgroupMatrix e h ρ M hM i hnil b) f) r s = ((Module.Basis.baseChange A b).repr (↑((kostantRootSubgroupPoints e h ρ M hM i hnil) f) ((Module.Basis.baseChange A b) s))) r

An entry of the root-subgroup matrix is the corresponding coordinate of the exponential action on a base-changed basis vector.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantRootSubgroupMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {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) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {η : Type u_2} [Fintype η] [DecidableEq η] (b : Module.Basis η ℤ ↥M) {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] (φ : A →+* B) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : (Matrix.GeneralLinearGroup.map φ) ((kostantRootSubgroupMatrix e h ρ M hM i hnil b) f) = (kostantRootSubgroupMatrix e h ρ M hM i hnil b) ((AlgHom.mapValue φ.toIntAlgHom) f)

The matrix-valued Kostant root subgroup is natural in the value ring.