The split maximal torus of a Kostant elementary group

Let U_ℤ = kostantForm e h act on a rational representation V through ρ and preserve an additive subgroup M ≤ V. A weight basis of M is an integral basis b : Basis η ℤ M each of whose vectors is a joint eigenvector of the designated Cartan operators ρ(hⱼ), with integer eigenvalues recorded by wt : η → κ → ℤ. Over any commutative ring A of points, the split torus 𝔾ₘ^κ then acts diagonally on A ⊗[ℤ] M: a point s : κ → Aˣ scales the basis vector b x by the value ∏ⱼ sⱼ ^ wt x j of the character wt x.

This is the split maximal torus of the pinning. What makes it a pinned torus rather than an arbitrary diagonal group is its interaction with the root subgroups. If the designated root vector eᵢ has weight α, meaning ⁅hⱼ, eᵢ⁆ = αⱼ eᵢ for every j, then

t(s) xᵢ(u) t(s)⁻¹ = xᵢ(α(s) u),

with α(s) = ∏ⱼ sⱼ ^ αⱼ the value at s of the same character. So the torus normalizes each root subgroup, acting on its parameter by the root, and consequently normalizes the whole elementary group E(A) = ⟨xᵢ(u)⟩. Nothing here divides by a factorial, so the equations hold over a value ring of any characteristic.

The same equation has an infinitesimal form. The designated root vector eᵢ restricts to the integral operator kostantRootOperator on M, the pinning's X_α; it raises weights by α, so a torus point conjugates it to α(s) X_α. This is kostantTorusPoints_conj_kostantRootOperator, the other half of what pins the root subgroups against the torus.

The analogous statement for the worked GLₙ example is TauCeti.GeneralLinear.diagonalTorusPoints_mul_rootSubgroupPoints_mul_inv; here the diagonal group is cut down to rank κ by the weight function, and the character by which it acts on a root subgroup is the root rather than a difference εᵢ - εⱼ of coordinates.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector: a joint eigenvector of the designated Cartan operators with prescribed integer eigenvalues.
• TauCeti.UniversalEnvelopingAlgebra.kostantCartanOperator: a designated Cartan vector as an integral operator on a Kostant-stable subgroup.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootOperator: a designated root vector as an integral operator on a Kostant-stable subgroup — the pinning's X_α.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints: the split torus of rank κ on the points of a Kostant-stable lattice presented in a weight basis.
• TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter: the cocharacter supported at one coordinate of the split torus.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubgroup: the image of that torus in the general linear group of the base-changed lattice.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusMatrix: the same action in matrix coordinates.

Main results

• TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.integralDividedPower: a divided power of a root vector of weight α raises the weight of a weight vector by a multiple of α.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_tmul_of_isCartanWeightVector: a torus point acts on a weight vector by the value of its character.
• TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter_tmul_basis: the coordinate cocharacter scales a weight vector by the corresponding coordinate of its weight.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_mul_inv_weylReflectTorusPoint: a torus point divided by its Weyl reflection is a value of the cocharacter supported at the reflecting index.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_injective: weights generating the whole character lattice make the torus a monomorphism on points.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusPoints: naturality in the value ring.
• TauCeti.UniversalEnvelopingAlgebra.mapScalarExtensionAutomorphisms_kostantTorusPoints: scalar extension of a torus point is the torus point with mapped parameter.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_conj_kostantRootSubgroupParam: the pinning equation t(s) xᵢ(u) t(s)⁻¹ = xᵢ(α(s) u).
• TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_coe_kostantRootOperator: the root operator raises weights by the root α.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_mul_baseChange_kostantRootOperator: the torus intertwines the root operator up to the value of the root, and TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_conj_kostantRootOperator is its conjugated form t(s) X_α t(s)⁻¹ = α(s) X_α.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_conj_kostantTorusPoints: the torus normalizes the elementary group.

References

• 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. C. Jantzen, Representations of Algebraic Groups, II.1.

Weight vectors

def TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (μ : κ → ℤ) (m : V) : Prop

A vector of V is a weight vector of weight μ when it is a joint eigenvector of the designated Cartan operators ρ(hⱼ) with the integer eigenvalues μ j.

Equations

• TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector h ρ μ m = ∀ (j : κ), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))) m = ↑(μ j) • m

theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {μ : κ → ℤ} {m : V} : IsCartanWeightVector h ρ μ m ↔ ∀ (j : κ), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))) m = ↑(μ j) • m

The pointwise characterization of a Cartan weight vector.

theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_iff_mem_eigenspace {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) {μ : κ → ℤ} {m : V} : IsCartanWeightVector h ρ μ m ↔ ∀ (j : κ), m ∈ (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))).eigenspace ↑(μ j)

Being a weight vector is joint membership in the eigenspaces of the Cartan operators.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.zero {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {h : κ → L} {ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V} (μ : κ → ℤ) : IsCartanWeightVector h ρ μ 0

Zero is a weight vector of every weight.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.add {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {h : κ → L} {ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V} {μ : κ → ℤ} {m n : V} (hm : IsCartanWeightVector h ρ μ m) (hn : IsCartanWeightVector h ρ μ n) : IsCartanWeightVector h ρ μ (m + n)

The sum of two weight vectors of the same weight has that weight.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.neg {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {h : κ → L} {ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V} {μ : κ → ℤ} {m : V} (hm : IsCartanWeightVector h ρ μ m) : IsCartanWeightVector h ρ μ (-m)

The negation of a weight vector has the same weight.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.sub {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {h : κ → L} {ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V} {μ : κ → ℤ} {m n : V} (hm : IsCartanWeightVector h ρ μ m) (hn : IsCartanWeightVector h ρ μ n) : IsCartanWeightVector h ρ μ (m - n)

The difference of two weight vectors of the same weight has that weight.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.smul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_2} {V : Type v} [AddCommGroup V] [Module ℚ V] {h : κ → L} {ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V} {μ : κ → ℤ} {m : V} (hm : IsCartanWeightVector h ρ μ m) (c : ℚ) : IsCartanWeightVector h ρ μ (c • m)

A rational multiple of a weight vector is a weight vector of the same weight.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.pow_rootVector {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} {i : ι} {α μ : κ → ℤ} {m : V} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (hm : IsCartanWeightVector h ρ μ m) (n : ℕ) : IsCartanWeightVector h ρ (μ + n • α) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) ^ n) m)

If the root vector eᵢ has weight α, then applying its action n times to a weight vector of weight μ produces a weight vector of weight μ + n α.

theorem TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector.integralDividedPower {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} {i : ι} {α μ : κ → ℤ} {m : V} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (hm : IsCartanWeightVector h ρ μ m) (n : ℕ) : IsCartanWeightVector h ρ (μ + n • α) (Associative.dividedPower n (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) • m)

If the root vector eᵢ has weight α, its n-th divided power raises the weight of a weight vector by n α. This is the statement that makes the torus act on a root subgroup through the root.

Cartan operators on a stable subgroup

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantCartanOperator {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) (j : κ) : Module.End ℤ ↥M

A designated Cartan vector acting on a Kostant-stable additive subgroup, as an integral operator. It is the restriction of ρ(hⱼ), which preserves M because hⱼ lies in the Kostant form.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantCartanOperator e h ρ M hM j = { toFun := fun (v : ↥M) => ⟨(ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))) ↑v, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantCartanOperator_apply {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) (j : κ) (v : ↥M) : ↑((kostantCartanOperator e h ρ M hM j) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h j))) ↑v

The integral Cartan operator acts by the ambient representation.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantCartanOperator_apply_of_isCartanWeightVector {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) {μ : κ → ℤ} {v : ↥M} (hv : IsCartanWeightVector h ρ μ ↑v) (j : κ) : (kostantCartanOperator e h ρ M hM j) v = μ j • v

On a weight vector the integral Cartan operator is multiplication by the integer weight.

theorem TauCeti.UniversalEnvelopingAlgebra.repr_kostantCartanOperator {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) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (j : κ) (m : ↥M) (y : η) : (b.repr ((kostantCartanOperator e h ρ M hM j) m)) y = wt y j * (b.repr m) y

In a weight basis, the integral Cartan operator is diagonal: it multiplies the y-th coordinate by wt y j.

theorem TauCeti.UniversalEnvelopingAlgebra.repr_eq_zero_of_isCartanWeightVector {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) {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) {μ : κ → ℤ} {m : ↥M} (hm : IsCartanWeightVector h ρ μ ↑m) {y : η} (hy : wt y ≠ μ) : (b.repr m) y = 0

A weight basis separates weights: a weight vector of weight μ has vanishing coordinates at every basis vector of a different weight.

Root operators on a stable subgroup

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootOperator {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) (i : ι) : Module.End ℤ ↥M

The designated root vector eᵢ acting on a Kostant-stable additive subgroup, as an integral operator.

It is the first restricted divided power of ρ(eᵢ), so it is the linear coefficient of the divided-power exponential defining the root subgroup, and it is the root vector X_α of the pinning.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootOperator e h ρ M hM i = TauCeti.integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M 1 ⋯

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantRootOperator_apply {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) (i : ι) (v : ↥M) : ↑((kostantRootOperator e h ρ M hM i) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑v

The integral root operator acts by the ambient representation of the root vector.

theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_coe_kostantRootOperator {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) (i : ι) {α μ : κ → ℤ} {v : ↥M} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (hv : IsCartanWeightVector h ρ μ ↑v) : IsCartanWeightVector h ρ (μ + α) ↑((kostantRootOperator e h ρ M hM i) v)

The integral root operator raises weights by the root: it is the first divided power of a root vector of weight α.

The split torus on points

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (A : Type u_3) [CommRing A] [Algebra ℤ A] : (κ → Aˣ) →* LinearMap.GeneralLinearGroup A (TensorProduct ℤ A ↥M)

The split maximal torus of rank κ on the A-points of a Kostant-stable lattice presented in a weight basis: the point s scales the base-changed basis vector b x by the value at s of the character wt x.

Equations

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubgroup {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (A : Type u_3) [CommRing A] [Algebra ℤ A] : Subgroup (LinearMap.GeneralLinearGroup A (TensorProduct ℤ A ↥M))

The image of the split weight torus in the general linear group of the base-changed lattice.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubgroup M b wt A = (TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints M b wt A).range

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubgroup_eq_range {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (A : Type u_3) [CommRing A] [Algebra ℤ A] : kostantTorusSubgroup M b wt A = (kostantTorusPoints M b wt A).range

The defining equation of kostantTorusSubgroup: it is the range of the torus points homomorphism, so Mathlib's MonoidHom.mem_range characterizes its elements.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_toLinearEquiv {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_3} [CommRing A] [Algebra ℤ A] (s : κ → Aˣ) : ((kostantTorusPoints M b wt A) s).toLinearEquiv = (basisWeightTorus (Module.Basis.baseChange A b) wt) s

The linear automorphism underlying a torus point is the diagonal weight automorphism.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_apply {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_3} [CommRing A] [Algebra ℤ A] (s : κ → Aˣ) (z : TensorProduct ℤ A ↥M) : ↑((kostantTorusPoints M b wt A) s) z = ((basisWeightTorus (Module.Basis.baseChange A b) wt) s) z

A torus point acts by the diagonal weight automorphism of the base-changed basis.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_injective {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_3} [CommRing A] [Algebra ℤ A] (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : Function.Injective ⇑(kostantTorusPoints M b wt A)

Spanning weights make the split torus a monomorphism on points. When the weights of the basis generate the whole character lattice, distinct torus points act differently on the base-changed lattice, over every value ring.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_tmul_basis {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_3} [CommRing A] [Algebra ℤ A] (s : κ → Aˣ) (a : A) (x : η) : ↑((kostantTorusPoints M b wt A) s) (a ⊗ₜ[ℤ] b x) = (↑(torusCharacter s (wt x)) * a) ⊗ₜ[ℤ] b x

A torus point scales a base-changed basis vector by the value of its weight character.

Coordinate cocharacters

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [DecidableEq κ] (A : Type u_3) [CommRing A] [Algebra ℤ A] (c : κ) : Aˣ →* LinearMap.GeneralLinearGroup A (TensorProduct ℤ A ↥M)

The cocharacter of the Kostant weight torus supported at the coordinate c. Its value at u scales a weight vector of weight μ by u ^ μ(c).

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter M b wt A c = (TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints M b wt A).comp (MonoidHom.mulSingle (fun (x : κ) => Aˣ) c)

theorem TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter_apply {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [DecidableEq κ] (A : Type u_3) [CommRing A] [Algebra ℤ A] (c : κ) (u : Aˣ) : (kostantCoordinateCocharacter M b wt A c) u = (kostantTorusPoints M b wt A) (Pi.mulSingle c u)

Evaluating the coordinate cocharacter at u gives the torus point supported at c.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter_tmul_basis {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [DecidableEq κ] (A : Type u_3) [CommRing A] [Algebra ℤ A] (c : κ) (u : Aˣ) (a : A) (x : η) : ↑((kostantCoordinateCocharacter M b wt A c) u) (a ⊗ₜ[ℤ] b x) = (↑(u ^ wt x c) * a) ⊗ₜ[ℤ] b x

The coordinate cocharacter scales a weight vector by the corresponding weight coordinate.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_mul_inv_weylReflectTorusPoint {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [DecidableEq κ] (A : Type u_3) [CommRing A] [Algebra ℤ A] (α : κ → ℤ) (c : κ) (s : κ → Aˣ) : (kostantTorusPoints M b wt A) s * ((kostantTorusPoints M b wt A) ((weylReflectTorusPoint α c) s))⁻¹ = (kostantCoordinateCocharacter M b wt A c) (torusCharacter s α)

A torus point divided by its Weyl reflection is a coordinate-cocharacter value. The reflection s_α changes only the c-th coordinate of a point, dividing it by the value α(s), so the quotient is the value at α(s) of the cocharacter supported at c. This is the image under the torus of TauCeti.mul_inv_weylReflectTorusPoint, the same identity in κ → Aˣ.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusPoints_tmul_basis {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] (φ : A →+* B) (s : κ → Aˣ) (a : A) (x : η) : (TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) (↑((kostantTorusPoints M b wt A) s) (a ⊗ₜ[ℤ] b x)) = ↑((kostantTorusPoints M b wt B) fun (j : κ) => (Units.map ↑φ) (s j)) ((TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) (a ⊗ₜ[ℤ] b x))

Naturality of the torus in the value ring, on a base-changed basis vector.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusPoints {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] (φ : A →+* B) (s : κ → Aˣ) (z : TensorProduct ℤ A ↥M) : (TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) (↑((kostantTorusPoints M b wt A) s) z) = ↑((kostantTorusPoints M b wt B) fun (j : κ) => (Units.map ↑φ) (s j)) ((TensorProduct.map φ.toIntAlgHom.toLinearMap LinearMap.id) z)

The torus on points is natural in the value ring.

theorem TauCeti.UniversalEnvelopingAlgebra.mapScalarExtensionAutomorphisms_kostantTorusPoints {κ : Type u_1} [Fintype κ] {V : Type v} [AddCommGroup V] (M : AddSubgroup V) {η : Type u_2} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A B : CommAlgCat ℤ} (φ : A ⟶ B) (s : κ → (↑A)ˣ) : (CategoryTheory.ConcreteCategory.hom (GeneralLinear.mapScalarExtensionAutomorphisms φ)) ((kostantTorusPoints M b wt ↑A) s) = (kostantTorusPoints M b wt ↑B) fun (j : κ) => (Units.map ↑(CommAlgCat.Hom.hom φ).toRingHom) (s j)

Scalar extension of a torus point. Extending the scalars of the torus point s along a morphism of value rings gives the torus point whose parameter is mapped into the target ring.

Matrix coordinates

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusMatrix {κ : Type u_1} {V : Type v} [AddCommGroup V] (M : AddSubgroup V) [Fintype κ] {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {A : Type u_2} [CommRing A] [Algebra ℤ A] : (κ → Aˣ) →* GL (Fin n) A

The torus attached to a weight basis, in the matrix coordinates of that basis.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.basisMatrix_kostantTorusPoints {κ : Type u_1} {V : Type v} [AddCommGroup V] (M : AddSubgroup V) [Fintype κ] {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {A : Type u_2} [CommRing A] [Algebra ℤ A] (s : κ → Aˣ) : (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv) ((kostantTorusPoints M b wt A) s) = (kostantTorusMatrix M b wt) s

Writing a Kostant torus point in the chosen basis gives kostantTorusMatrix.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusMatrix_apply {κ : Type u_1} {V : Type v} [AddCommGroup V] (M : AddSubgroup V) [Fintype κ] {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {A : Type u_2} [CommRing A] [Algebra ℤ A] (s : κ → Aˣ) : (kostantTorusMatrix M b wt) s = diagGL fun (i : Fin n) => torusCharacter s (wt i)

In a weight basis, a torus point is the diagonal matrix of its weight characters.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusMatrix {κ : Type u_1} {V : Type v} [AddCommGroup V] (M : AddSubgroup V) [Fintype κ] {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {A : Type u_2} [CommRing A] [Algebra ℤ A] {B : Type u_3} [CommRing B] [Algebra ℤ B] (φ : A →+* B) (s : κ → Aˣ) : (Matrix.GeneralLinearGroup.map φ) ((kostantTorusMatrix M b wt) s) = (kostantTorusMatrix M b wt) fun (j : κ) => (Units.map ↑φ) (s j)

The matrix torus is natural in the value ring. Applying a ring homomorphism entrywise to a torus point written in a weight basis gives the torus point of the transported parameters. The p ^ k-power Frobenius is the case TauCeti.UniversalEnvelopingAlgebra.map_iterateFrobenius_kostantTorusMatrix.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_tmul_of_isCartanWeightVector {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) [Fintype κ] {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_4} [CommRing A] [Algebra ℤ A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) {μ : κ → ℤ} {m : ↥M} (hm : IsCartanWeightVector h ρ μ ↑m) (s : κ → Aˣ) (a : A) : ↑((kostantTorusPoints M b wt A) s) (a ⊗ₜ[ℤ] m) = (↑(torusCharacter s μ) * a) ⊗ₜ[ℤ] m

A torus point acts on a weight vector by the value of the corresponding character.

The pinning equation

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_mul_kostantRootSubgroupPoints {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) [Fintype κ] {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_4} [CommRing A] [Algebra ℤ A] (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) {i : ι} {α : κ → ℤ} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (s : κ → Aˣ) (f g : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (hg : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g) = ↑(torusCharacter s α) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f)) : (kostantTorusPoints M b wt A) s * (kostantRootSubgroupPoints e h ρ M hM i hnil) f = (kostantRootSubgroupPoints e h ρ M hM i hnil) g * (kostantTorusPoints M b wt A) s

The pinning equation for the torus and a root subgroup. If the designated root vector eᵢ has weight α, then the torus point s conjugates the root-subgroup element with parameter u into the one with parameter α(s) u.

The pinning equation for the root vector

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_mul_baseChange_kostantRootOperator {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) [Fintype κ] {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_4} [CommRing A] [Algebra ℤ A] (i : ι) {α : κ → ℤ} (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (s : κ → Aˣ) : ↑((kostantTorusPoints M b wt A) s) * LinearMap.baseChange A (kostantRootOperator e h ρ M hM i) = ↑(torusCharacter s α) • (LinearMap.baseChange A (kostantRootOperator e h ρ M hM i) * ↑((kostantTorusPoints M b wt A) s))

The torus acts on the root operator through the root. A torus point intertwines the base-changed root operator with itself, up to the value α(s) of the root.

This is the infinitesimal form of the pinning equation kostantTorusPoints_conj_kostantRootSubgroupParam.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_conj_kostantRootOperator {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) [Fintype κ] {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) {A : Type u_4} [CommRing A] [Algebra ℤ A] (i : ι) {α : κ → ℤ} (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (s : κ → Aˣ) : ↑((kostantTorusPoints M b wt A) s) * LinearMap.baseChange A (kostantRootOperator e h ρ M hM i) * ↑((kostantTorusPoints M b wt A) s)⁻¹ = ↑(torusCharacter s α) • LinearMap.baseChange A (kostantRootOperator e h ρ M hM i)

The pinning relation for the root vector, in conjugated form: t(s) X_α t(s)⁻¹ is α(s) X_α. It says that the tangent vector of the root subgroup lies in the α-weight space of the adjoint action of the split maximal torus.

The torus inside the elementary group

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusPoints_conj_kostantRootSubgroupParam {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) [Fintype κ] {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) {i : ι} {α : κ → ℤ} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : CommAlgCat ℤ) (s : κ → (↑A)ˣ) (t : Multiplicative ↑A) : (kostantTorusPoints M b wt ↑A) s * (kostantRootSubgroupParam e h ρ M hM i hnil A) t * ((kostantTorusPoints M b wt ↑A) s)⁻¹ = (kostantRootSubgroupParam e h ρ M hM i hnil A) (Multiplicative.ofAdd (↑(torusCharacter s α) * Multiplicative.toAdd t))

The pinning equation with the parameter read in the value ring. Conjugation by the torus point s carries the root-subgroup element xᵢ(u) to xᵢ(α(s) u), where α is the weight of the root vector eᵢ.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_conj_kostantTorusPoints {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) [Fintype κ] {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) (hwt : ∀ (x : η), IsCartanWeightVector h ρ (wt x) ↑(b x)) (α : ι → κ → ℤ) (hα : ∀ (i : ι) (j : κ), ⁅h j, e i⁆ = ↑(α i j) • e i) (hnil : ∀ (i : ι), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : CommAlgCat ℤ) (s : κ → (↑A)ˣ) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj ((kostantTorusPoints M b wt ↑A) s))) (kostantElementarySubgroup e h ρ M hM hnil A) = kostantElementarySubgroup e h ρ M hM hnil A

The torus normalizes the elementary group. Conjugation by a torus point permutes the root subgroups, acting on the parameter of the i-th one through the root α i, so it carries the group they generate onto itself.