The type-G₂ relation for Kostant root-subgroup scheme morphisms

This file transports the integral type-G₂ root-string identity to the scheme-valued points of the represented Kostant root-subgroup morphisms xᵢ : 𝔾ₐ ⟶ GLₙ. Suppose six distinguished root vectors follow the positive root string

α, β, α + β, 2α + β, 3α + β, 3α + 2β.

If their scaled brackets have the integral coefficients c, d, a, and b specified in the statements below, then on points over every commutative ring A one has

xα(t) xβ(u) = xβ(u) x_{α+β}(c t u) x_{2α+β}(d t² u)
  x_{3α+β}(a t³ u) x_{3α+2β}(b t³ u²) xα(t).

The represented scheme morphisms are compared with their divided-power actions through schemePointsMulEquiv_kostantRootSubgroup. Applying the matrix-coordinate homomorphism to kostantRootSubgroupPoints_mul_of_lie_eq_three_nsmul then proves the relation in GLₙ(A). No factorial is inverted, so the result remains valid in characteristics two and three.

Main results

• schemePointsMulEquiv_kostantRootSubgroup_mul_of_lie_eq_three_nsmul gives the product relation for four supplied output points.
• schemePointsMulEquiv_kostantRootSubgroup_mul_of_lie_eq_three_nsmul' writes those output points explicitly.

References

• R. W. Carter, Simple Groups of Lie Type, Theorem 5.2.2.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§25–26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

theorem TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_kostantRootSubgroup_mul_of_lie_eq_three_nsmul {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 : ∀ x ∈ kostantForm e h, ∀ v ∈ M, (ρ x) v ∈ M) {n : ℕ} (basis : Module.Basis (Fin n) ℤ ↥M) (A : Type) [CommRing A] {i j k l m o : I} {c d a b : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : c • ⁅e i, e k⁆ = (2 * d) • e l) (hil : d • ⁅e i, e l⁆ = (3 * a) • e m) (hlk : (d * c) • ⁅e l, e k⁆ = (3 * b) • e o) (him : ⁅e i, e m⁆ = 0) (hio : ⁅e i, e o⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hlm : ⁅e l, e m⁆ = 0) (hko : ⁅e k, e o⁆ = 0) (hlo : ⁅e l, e o⁆ = 0) (hmo : ⁅e m, e o⁆ = 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)))) (ho : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e o)))) (f g p q r s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) (hp : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) = ↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))) (hq : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q) = ↑d * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))) (hr : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) r) = ↑a * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))) (hs : Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) s) = ↑b * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g) ^ 2)) : (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp f (kostantRootSubgroup e h ρ M hM i hi basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp g (kostantRootSubgroup e h ρ M hM j hj basis).hom.hom) = (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp g (kostantRootSubgroup e h ρ M hM j hj basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (kostantRootSubgroup e h ρ M hM k hk basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp q (kostantRootSubgroup e h ρ M hM l hl basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp r (kostantRootSubgroup e h ρ M hM m hm basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp s (kostantRootSubgroup e h ρ M hM o ho basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp f (kostantRootSubgroup e h ρ M hM i hi basis).hom.hom)

The type-G₂ product relation on scheme-valued points of represented Kostant root subgroups. The indices i, j, k, l, m, o correspond to α, β, α + β, 2α + β, 3α + β, 3α + 2β. The four supplied output points have parameters c t u, d t² u, a t³ u, and b t³ u².

theorem TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_kostantRootSubgroup_mul_of_lie_eq_three_nsmul' {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 : ∀ x ∈ kostantForm e h, ∀ v ∈ M, (ρ x) v ∈ M) {n : ℕ} (basis : Module.Basis (Fin n) ℤ ↥M) (A : Type) [CommRing A] {i j k l m o : I} {c d a b : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : c • ⁅e i, e k⁆ = (2 * d) • e l) (hil : d • ⁅e i, e l⁆ = (3 * a) • e m) (hlk : (d * c) • ⁅e l, e k⁆ = (3 * b) • e o) (him : ⁅e i, e m⁆ = 0) (hio : ⁅e i, e o⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hlm : ⁅e l, e m⁆ = 0) (hko : ⁅e k, e o⁆ = 0) (hlo : ⁅e l, e o⁆ = 0) (hmo : ⁅e m, e o⁆ = 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)))) (ho : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e o)))) (f g : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp f (kostantRootSubgroup e h ρ M hM i hi basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp g (kostantRootSubgroup e h ρ M hM j hj basis).hom.hom) = (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp g (kostantRootSubgroup e h ρ M hM j hj basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))))) (kostantRootSubgroup e h ρ M hM k hk basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑d * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))))) (kostantRootSubgroup e h ρ M hM l hl basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑a * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g))))) (kostantRootSubgroup e h ρ M hM m hm basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑b * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g) ^ 2)))) (kostantRootSubgroup e h ρ M hM o ho basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp f (kostantRootSubgroup e h ρ M hM i hi basis).hom.hom)

The type-G₂ product relation on scheme-valued points with the four output points written explicitly at parameters c t u, d t² u, a t³ u, and b t³ u².