Scheme morphisms from Kostant root subgroups

Let a Kostant integral form act on a rational representation, preserving an integral lattice M. A finite basis of M turns the divided-power exponential attached to a nilpotent root vector into a natural family of homomorphisms

𝔾ₐ(A) → GLₙ(A).

The associated polynomial comodule determines a coordinate Hopf-algebra morphism O(GLₙ) → O(𝔾ₐ). Relative spectrum then gives a genuine affine group-scheme morphism 𝔾ₐ → GLₙ over ℤ. This file proves that its action on points is exactly the original Kostant exponential matrix.

Integral PBW must still produce the finite free admissible lattices used by the Chevalley--Demazure construction. The results here apply once such a lattice and basis are given. The representation carrier is universe-zero because the current group-scheme reconstruction API requires the base, coordinate Hopf algebra, and comodule to inhabit the same universe.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap: the coordinate Hopf-algebra morphism represented by the Kostant polynomial coaction.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroup: the affine group-scheme morphism 𝔾ₐ → GLₙ.
• TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_kostantRootSubgroupCoordinateMap: the induced matrix is the original Kostant exponential matrix.
• TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_kostantRootSubgroup: the same compatibility for scheme-valued points.

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.kostantRootSubgroupCoordinateMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) : GeneralLinear.coordinateHopfAlgebra ℤ n ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The coordinate Hopf-algebra morphism of the Kostant root subgroup in the basis b.

It sends the generic matrix to the coefficient matrix of the finite polynomial comodule kostantRootSubgroupComodule.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b = CommHopfAlgCat.ofHom (TauCeti.Comodule.coordinateBialgHom b)

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap_X {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (r s : Fin n) : (CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b)) ((GeneralLinear.coordinateHopfAlgebraAlgEquiv ℤ n) ((GeneralLinear.coordinateRingMap ℤ n) (MvPolynomial.X (r, s)))) = Comodule.coefficientMatrix b r s

A generic matrix coordinate pulls back to the corresponding matrix coefficient of the Kostant polynomial comodule.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) : AdditiveGroup.groupScheme ℤ ⟶ GeneralLinear.groupScheme ℤ n

The affine group-scheme morphism 𝔾ₐ → GLₙ represented by the Kostant divided-power exponential in the basis b.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroup e h ρ M hM i hnil b = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (TauCeti.Comodule.coordinateGroupSchemeHom b)

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroup_def {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) : kostantRootSubgroup e h ρ M hM i hnil b = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧ℤ).map (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b).op) (CategoryTheory.eqToHom ⋯))

The Kostant root subgroup is relative spectrum applied contravariantly to its coordinate Hopf-algebra morphism, transported across the named presentation of 𝔾ₐ.

theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_kostantRootSubgroupCoordinateMap_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)) (r s : Fin n) : ↑((GeneralLinear.pointsMulEquiv n) (WithConv.toConv (q.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b))))) r s = ((Module.Basis.baseChange A b).repr (↑((kostantRootSubgroupPoints e h ρ M hM i hnil) q) ((Module.Basis.baseChange A b) s))) r

On algebra-valued points, precomposition with the Kostant coordinate morphism gives the original divided-power exponential matrix.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_kostantRootSubgroupCoordinateMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)) : GeneralLinear.pointToGeneralLinear n (WithConv.toConv (q.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil b)))) = (kostantRootSubgroupMatrix e h ρ M hM i hnil b) q

On algebra-valued points, the matrix induced by the Kostant coordinate morphism is the original divided-power exponential matrix.

theorem TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_kostantRootSubgroup_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type) [CommRing A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) (r s : Fin n) : ↑((GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (kostantRootSubgroup e h ρ M hM i hnil b).hom.hom)) r s = ((Module.Basis.baseChange A b).repr (↑((kostantRootSubgroupPoints e h ρ M hM i hnil) ((AdditiveGroup.groupSchemePointMulEquiv A).symm p)) ((Module.Basis.baseChange A b) s))) r

On scheme-valued points, the represented Kostant root subgroup is exactly the divided-power exponential matrix in the basis b.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_kostantRootSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type u_1} {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) (i : I) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type) [CommRing A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (kostantRootSubgroup e h ρ M hM i hnil b).hom.hom) = (kostantRootSubgroupMatrix e h ρ M hM i hnil b) ((AdditiveGroup.groupSchemePointMulEquiv A).symm p)

On scheme-valued points, the represented Kostant root subgroup is the original divided-power exponential matrix in the basis b.