Diagonal split-torus representations and the Kostant weight torus

A basis b of an integral module together with weights wt gives a diagonal representation of the split torus 𝔾ₘ^κ: a point s : κ → Aˣ scales the basis vector b x by the value ∏ⱼ sⱼ ^ wt x j of its weight character. This file packages that representation as a morphism of affine group schemes over ℤ,

𝔾ₘ^κ ⟶ GLₙ,

by reading the weights as characters of the split torus and taking the associated diagonal representation. When b and wt are the weight data used by TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints, the two descriptions agree on points of every value ring, so all the pinning equations proved for that point action — in particular kostantTorusPoints_conj_kostantRootSubgroupParam, the conjugation formula t(s) xᵢ(u) t(s)⁻¹ = xᵢ(α(s) u) — are statements about this morphism.

When the weights span the lattice of exponent vectors the representation is faithful, and the source torus is then represented as a closed subgroup scheme of GLₙ. Identifying this closed subgroup with a maximal torus of a Chevalley group requires the appropriate Kostant lattice, Cartan weights, and ambient-group construction; those hypotheses are not part of the declarations in this file.

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

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_weightTorus_eq_kostantTorusMatrix: composing a scheme-valued torus point with the represented weight torus gives the matrix of the existing Kostant torus action.
• TauCeti.UniversalEnvelopingAlgebra.weightTorusRepresentation: the diagonal representation morphism of affine group schemes 𝔾ₘ^κ ⟶ GLₙ.
• TauCeti.UniversalEnvelopingAlgebra.weightTorusClosedSubgroup: the resulting closed subgroup scheme of GLₙ when the weights span.

Main results

• schemePointsMulEquiv_comp_weightTorusRepresentation_apply: the named scheme morphism induces the diagonal action kostantTorusPoints on scheme-valued points.
• TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_weightTorusRepresentation: spanning weights make the representation a closed immersion.

References

• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• J. S. Milne, Algebraic Groups (2017), §12.c.

theorem TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_weightTorus_eq_kostantTorusMatrix {κ : Type} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (A : Type) [CommRing A] [Algebra ℤ A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ κ).X) : (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (GeneralLinear.weightTorus wt).hom.hom) = (kostantTorusMatrix M b wt) (SplitTorus.schemePointsMulEquiv p)

Scheme-valued points of the represented weight torus are exactly the matrices of the pointwise Kostant torus action in the given weight basis.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.weightTorusRepresentation {κ M : Type} [AddCommMonoid M] [Module ℤ M] {n : ℕ} (b : Module.Basis (Fin n) ℤ M) (wt : Fin n → κ → ℤ) [Fintype κ] : SplitTorus.groupScheme ℤ κ ⟶ GeneralLinear.groupScheme ℤ n

The diagonal representation of a split torus attached to a basis and its weights, as a morphism of affine group schemes 𝔾ₘ^κ ⟶ GLₙ over ℤ.

It is the diagonal representation of the split torus whose weight characters are the weights of the basis.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.weightTorusRepresentation_def {κ M : Type} [AddCommMonoid M] [Module ℤ M] {n : ℕ} (b : Module.Basis (Fin n) ℤ M) (wt : Fin n → κ → ℤ) [Fintype κ] : weightTorusRepresentation b wt = DiagonalizableGroup.diagonalGroupSchemeHom (SplitTorus.characterGroup κ) b fun (x : Fin n) => SplitTorus.weightCharacter (wt x)

The weight-torus representation is the general diagonalizable-group representation specialized to the character lattice of a split torus.

theorem TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_weightTorusRepresentation {κ M : Type} [AddCommMonoid M] [Module ℤ M] {n : ℕ} (b : Module.Basis (Fin n) ℤ M) (wt : Fin n → κ → ℤ) [Fintype κ] (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (weightTorusRepresentation b wt).hom.hom)

A weight basis whose weights span the lattice of exponent vectors presents the split torus as a closed subgroup of GLₙ.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.weightTorusClosedSubgroup {κ M : Type} [AddCommMonoid M] [Module ℤ M] {n : ℕ} (b : Module.Basis (Fin n) ℤ M) (wt : Fin n → κ → ℤ) [Fintype κ] (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : ClosedSubgroupScheme (GeneralLinear.groupScheme ℤ n)

The split torus represented by a weight basis with spanning weights, as a closed subgroup scheme of GLₙ. This does not assert maximality in an ambient reductive group.

Equations

• TauCeti.UniversalEnvelopingAlgebra.weightTorusClosedSubgroup b wt hwt = TauCeti.ClosedSubgroupScheme.mk (TauCeti.UniversalEnvelopingAlgebra.weightTorusRepresentation b wt)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_weightTorusClosedSubgroup {κ M : Type} [AddCommMonoid M] [Module ℤ M] {n : ℕ} (b : Module.Basis (Fin n) ℤ M) (wt : Fin n → κ → ℤ) [Fintype κ] (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : have x := ⋯; ↑(weightTorusClosedSubgroup b wt hwt) = CategoryTheory.Subobject.mk (weightTorusRepresentation b wt)

The underlying subobject of the closed weight torus is represented by its defining closed immersion.

theorem TauCeti.UniversalEnvelopingAlgebra.pointToGeneralLinear_comp_diagonalCoordinateMap_eq_kostantTorusPoints_apply {κ : Type} {n : ℕ} (wt : Fin n → κ → ℤ) [Fintype κ] {V : Type} [AddCommGroup V] (L : AddSubgroup V) (bL : Module.Basis (Fin n) ℤ ↥L) (A : Type) [CommRing A] (q : WithConv (MonoidAlgebra ℤ (Multiplicative (κ →₀ ℤ)) →ₐ[ℤ] A)) (i j : Fin n) : ↑(GeneralLinear.pointToGeneralLinear n (WithConv.toConv (q.ofConv.comp ↑(DiagonalizableGroup.diagonalCoordinateMap bL fun (x : Fin n) => SplitTorus.weightCharacter (wt x))))) i j = ((Module.Basis.baseChange A bL).repr (↑((kostantTorusPoints L bL wt A) (SplitTorus.pointsMulEquiv q)) ((Module.Basis.baseChange A bL) j))) i

On points, the represented split torus is the original diagonal action. The matrix of the point q of 𝔾ₘ^κ in the basis bL is the matrix of kostantTorusPoints at the coordinate family of q.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_comp_weightTorusRepresentation_apply {κ : Type} {n : ℕ} (wt : Fin n → κ → ℤ) [Fintype κ] {V : Type} [AddCommGroup V] (L : AddSubgroup V) (bL : Module.Basis (Fin n) ℤ ↥L) (A : Type) [CommRing A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ κ).X) (i j : Fin n) : ((GeneralLinear.groupSchemePointMulEquiv n A).symm (CategoryTheory.CategoryStruct.comp p (weightTorusRepresentation bL wt).hom.hom)).ofConv ((GeneralLinear.coordinateHopfAlgebraAlgEquiv ℤ n) ((GeneralLinear.coordinateRingMap ℤ n) (MvPolynomial.X (i, j)))) = ((Module.Basis.baseChange A bL).repr (↑((kostantTorusPoints L bL wt A) (SplitTorus.schemePointsMulEquiv p)) ((Module.Basis.baseChange A bL) j))) i

On scheme-valued points, the named weight-torus representation induces the diagonal action kostantTorusPoints associated to the same basis and weight data.