The G₂ short-pair relation for Kostant root subgroups

For the roots α, α + β, 2α + β, 3α + β, 3α + 2β, the scaled brackets [eᵢ,eⱼ] = 2c eₖ, c[eᵢ,eₖ] = 3d eₗ, and c[eₖ,eⱼ] = 3a eₘ give

xᵢ(t) xⱼ(u) = xⱼ(u) xₖ(2ctu) xₗ(3dt²u) xₘ(3atu²) xᵢ(t).

The six vanishing brackets are listed explicitly in the theorem. The parameters belong to an arbitrary commutative ring, so the relation includes characteristics two and three. The integral coefficients allow different choices of signs for the distinguished root vectors.

This is the Kostant-lattice form of baseChangeExp_mul_baseChangeExp_of_g2_short_pair and the short-pair input for the relations of the represented root-subgroup morphisms.

References

• R. W. Carter, Simple Groups of Lie Type, §4.2 and Theorem 5.2.2.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_mul_of_g2_short_pair {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 : ∀ x ∈ kostantForm e h, ∀ v ∈ M, (ρ x) v ∈ M) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k l m : ι} {c d a : ℤ} (hij : ⁅e i, e j⁆ = (2 * c) • e k) (hik : c • ⁅e i, e k⁆ = (3 * d) • e l) (hkj : c • ⁅e k, e j⁆ = (3 * a) • e m) (hil : ⁅e i, e l⁆ = 0) (him : ⁅e i, e m⁆ = 0) (hjm : ⁅e j, e m⁆ = 0) (hkl : ⁅e k, e l⁆ = 0) (hkm : ⁅e k, e m⁆ = 0) (hlm : ⁅e l, e m⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (hl : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e l)))) (hm : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e m)))) (f g p q r : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (hp : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv p) = ↑c * (2 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) (hq : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv q) = ↑d * (3 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 2 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) (hr : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv r) = ↑a * (3 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g) ^ 2)) : (kostantRootSubgroupPoints e h ρ M hM i hi) f * (kostantRootSubgroupPoints e h ρ M hM j hj) g = (kostantRootSubgroupPoints e h ρ M hM j hj) g * (kostantRootSubgroupPoints e h ρ M hM k hk) p * (kostantRootSubgroupPoints e h ρ M hM l hl) q * (kostantRootSubgroupPoints e h ρ M hM m hm) r * (kostantRootSubgroupPoints e h ρ M hM i hi) f

The G₂ short-pair product relation on an admissible Kostant lattice, with the three output points supplied at parameters 2ctu, 3dt²u, and 3atu². The indices i, j, k, l, m correspond to α, α + β, 2α + β, 3α + β, 3α + 2β.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_mul_of_g2_short_pair' {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 : ∀ x ∈ kostantForm e h, ∀ v ∈ M, (ρ x) v ∈ M) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k l m : ι} {c d a : ℤ} (hij : ⁅e i, e j⁆ = (2 * c) • e k) (hik : c • ⁅e i, e k⁆ = (3 * d) • e l) (hkj : c • ⁅e k, e j⁆ = (3 * a) • e m) (hil : ⁅e i, e l⁆ = 0) (him : ⁅e i, e m⁆ = 0) (hjm : ⁅e j, e m⁆ = 0) (hkl : ⁅e k, e l⁆ = 0) (hkm : ⁅e k, e m⁆ = 0) (hlm : ⁅e l, e m⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (hl : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e l)))) (hm : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e m)))) (f g : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : (kostantRootSubgroupPoints e h ρ M hM i hi) f * (kostantRootSubgroupPoints e h ρ M hM j hj) g = (kostantRootSubgroupPoints e h ρ M hM j hj) g * (kostantRootSubgroupPoints e h ρ M hM k hk) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑c * (2 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))))) * (kostantRootSubgroupPoints e h ρ M hM l hl) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑d * (3 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 2 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))))) * (kostantRootSubgroupPoints e h ρ M hM m hm) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑a * (3 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g) ^ 2)))) * (kostantRootSubgroupPoints e h ρ M hM i hi) f

The G₂ short-pair product relation on an admissible Kostant lattice, with the three output points written explicitly at parameters 2ctu, 3dt²u, and 3atu².