Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Commutator.G2

The type-G₂ commutator relation for Kostant root subgroups #

This file transports the integral type-G₂ exponential identity to the Kostant root subgroups attached to an admissible lattice. Suppose six distinguished root vectors follow the positive root string

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

Write c, d, a, and b for the integral coefficients of the last four vectors in the successive divided brackets. The hypotheses below say directly that these scaled brackets have the normalizations required by the integral straightening rule:

[eα, eβ]       = c e_{α+β},
c [eα,e_{α+β}] = 2d e_{2α+β},
d [eα,e_{2α+β}] = 3a e_{3α+β},
dc [e_{2α+β},e_{α+β}] = 3b e_{3α+2β}.

They also require the vanishing brackets

[eα,e_{3α+β}] = [eα,e_{3α+2β}] = [eβ,e_{α+β}] = 0,
[e_{2α+β},e_{3α+β}] = [e_{α+β},e_{3α+2β}] = 0,
[e_{2α+β},e_{3α+2β}] = [e_{3α+β},e_{3α+2β}] = 0.

The resulting relation is

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).

No factorial is inverted in the value ring. Thus the formula is valid in characteristics two and three as well as in characteristic zero. Together with the commuting, class-two, and length-two relations in Commutator.Basic, this supplies one exceptional rank-two pointwise Chevalley relation needed by the integral Chevalley--Demazure construction. The remaining type-G₂ configuration, the pair α, α + β, is not transported here; see TauCeti.RingTheory.DividedPowers.RootString.G2 for the integral identity it needs.

Main results #

References #

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_mul_of_lie_eq_three_nsmul {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 : xkostantForm e h, vM, (ρ x) v M) {A : Type u_2} [CommRing A] [Algebra A] {i j k l m o : ι} {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 : WithConv (SymmetricAlgebra →ₐ[] A)) (hp : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv p) = c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) (hq : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv q) = d * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 2 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) (hr : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv r) = a * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 3 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) (hs : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv s) = b * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 3 * 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 o ho) s * (kostantRootSubgroupPoints e h ρ M hM i hi) f

The type-G₂ Chevalley commutator relation for Kostant root subgroups. The indices i, j, k, l, m, o correspond respectively to the roots α, β, α + β, 2α + β, 3α + β, 3α + 2β. The four supplied points have parameters c t u, d t² u, a t³ u, and b t³ u². Besides the four displayed scaled bracket relations, the hypotheses require the seven brackets between i,m; i,o; j,k; l,m; k,o; l,o; and m,o to vanish.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_mul_of_lie_eq_three_nsmul' {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 : xkostantForm e h, vM, (ρ x) v M) {A : Type u_2} [CommRing A] [Algebra A] {i j k l m o : ι} {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 : WithConv (SymmetricAlgebra →ₐ[] A)) :

The type-G₂ Chevalley commutator relation with the four additional root-subgroup points written explicitly at parameters c t u, d t² u, a t³ u, and b t³ u².

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_conj_of_lie_eq_three_nsmul {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 : xkostantForm e h, vM, (ρ x) v M) {A : Type u_2} [CommRing A] [Algebra A] {i j k l m o : ι} {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 : WithConv (SymmetricAlgebra →ₐ[] A)) (hp : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv p) = c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) (hq : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv q) = d * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 2 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) (hr : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv r) = a * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 3 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) (hs : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv s) = b * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 3 * 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 i hi) f)⁻¹ = (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 o ho) s

The conjugation form of the type-G₂ Chevalley relation. Conjugating the β-root subgroup by the α-root subgroup produces the four positive-root factors at parameters c t u, d t² u, a t³ u, and b t³ u².

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_conj_of_lie_eq_three_nsmul' {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 : xkostantForm e h, vM, (ρ x) v M) {A : Type u_2} [CommRing A] [Algebra A] {i j k l m o : ι} {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 : WithConv (SymmetricAlgebra →ₐ[] A)) :

The conjugation form of the type-G₂ Chevalley relation with all four additional root-subgroup points written explicitly.