The matrix of a cube-zero root subgroup

The matrix of a Kostant root subgroup at parameter t is the divided-power exponential ∑ₖ tᵏ e⁽ᵏ⁾ of the root operator, read in the chosen lattice basis. When the operator squares to zero this is 1 + t X for the integral matrix X of the operator, which is TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_one_add_smul. This file treats the next case, an operator that cubes to zero, where one more term survives:

xᵢ(t) = 1 + t X + t² Y,

Y being the integral matrix of the divided square e⁽²⁾ = e² / 2 on the lattice. This is the shape of a simple root subgroup acting through a three-term weight string, such as a short root subgroup of type G₂ on the seven-dimensional module. The equation is proved on every algebra-valued point and then read on the coordinate morphism, where it lets a consumer check a matrix equation on all points of the root subgroup at once.

Main results

Both live in the namespace TauCeti.UniversalEnvelopingAlgebra.

• kostantRootSubgroupMatrix_eq_one_add_smul_add_smul: the matrix of a cube-zero root subgroup at a point is 1 + t X + t² Y.
• map_genericMatrix_kostantRootSubgroupCoordinateMap_eq_one_add_smul_add_smul: the same equation on the generic matrix, along the root-subgroup coordinate morphism.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_one_add_smul_add_smul {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] (X X₂ : Matrix η η ℤ) (hclass : nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ≤ 3) (haction : ∀ (s : η), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = ∑ r : η, X r s • ↑(b r)) (haction₂ : ∀ (s : η), (Associative.dividedPower 2 (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) ↑(b s) = ∑ r : η, X₂ r s • ↑(b r)) (f : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : ↑((kostantRootSubgroupMatrix e h ρ M hM i hnil b) f) = 1 + Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) • X.map Int.cast + Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 2 • X₂.map Int.cast

The matrix of a cube-zero root subgroup is 1 + t X + t² X₂. When the root operator cubes to zero its divided-power exponential stops after the quadratic term.

theorem TauCeti.UniversalEnvelopingAlgebra.map_genericMatrix_kostantRootSubgroupCoordinateMap_eq_one_add_smul_add_smul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type} [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)))) {N : ℕ} (bb : Module.Basis (Fin N) ℤ ↥M) (X Y : Matrix (Fin N) (Fin N) ℤ) (hclass : nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ≤ 3) (haction : ∀ (s : Fin N), (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(bb s) = ∑ r : Fin N, X r s • ↑(bb r)) (hsquare : ∀ (s : Fin N), (Associative.dividedPower 2 (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) ↑(bb s) = ∑ r : Fin N, Y r s • ↑(bb r)) : (GeneralLinear.genericMatrix ℤ N).map ⇑↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i hnil bb)) = 1 + (SymmetricAlgebra.ι ℤ ℤ) 1 • X.map Int.cast + (SymmetricAlgebra.ι ℤ ℤ) 1 ^ 2 • Y.map Int.cast

The generic matrix of a cube-zero root subgroup is 1 + t X + t² Y. This is TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_eq_one_add_smul_add_smul read on the coordinate morphism rather than on a point: the entries of the generic matrix of GL N are carried to those of 1 + t X + t² Y for the parameter t of the universal point of 𝔾ₐ.