Documentation

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

Chevalley commutator relations for Kostant root subgroups #

Let U_ℤ = kostantForm e h act on a rational vector space V through ρ, let M ≤ V be a U_ℤ-stable additive subgroup, and let eᵢ, eⱼ, eₖ be distinguished root vectors with nilpotent images. If

⁅eᵢ, eⱼ⁆ = c • eₖ,   ⁅eᵢ, eₖ⁆ = 0,   ⁅eⱼ, eₖ⁆ = 0

for an integer c — the situation of two roots α, β with α + β a root but neither 2α + β nor α + 2β a root, c being the Chevalley structure constant N_{α β} — then the root subgroups on the points of M ⊗ A satisfy the Chevalley commutator relation

x_α(t) x_β(u) x_α(t)⁻¹ = x_β(u) x_{α+β}(c t u).

This is the case of the Chevalley commutator formula in which only one further root subgroup occurs; in a simply-laced root system every pair of non-proportional roots falls under it or under the commuting case. The relation holds over every commutative ring A, with no factorial inverted, because it descends from the coefficient-one normal-ordering rule for divided powers.

The multiply-laced types B, C, and F₄ also produce pairs α, β for which 2α + β is a root. There the second bracket no longer vanishes: instead

⁅eᵢ, eⱼ⁆ = c • eₖ,   ⁅eᵢ, ⁅eᵢ, eⱼ⁆⁆ = (2 * d) • e_l,   ⁅eᵢ, e_l⁆ = ⁅eⱼ, eₖ⁆ = ⁅eₖ, e_l⁆ = 0,

the factor 2 being what makes (ad eᵢ)² eⱼ / 2 integral, and the relation acquires one more factor:

x_α(t) x_β(u) x_α(t)⁻¹ = x_β(u) x_{α+β}(c t u) x_{2α+β}(d t² u).

Type G₂ additionally needs the longer chain with factors at 3α + β and 3α + 2β; its transport to Kostant root subgroups is in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Commutator.G2.Basic.

The general statements about integral nilpotent exponentials are TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq and TauCeti.baseChangeExp_mul_baseChangeExp_of_commutator_eq_two_nsmul; this file only supplies the Lie-theoretic hypotheses and transports the identities to the root subgroups in LinearMap.GeneralLinearGroup.

Main results #

References #

source
theorem TauCeti.UniversalEnvelopingAlgebra.dividedPower_zsmul_apply_mem {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) (c : ℤ) (k : ι) (n : ℕ) (v : V) :
v ∈ M → Associative.dividedPower n (c • ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k))) • v ∈ M

A Kostant-stable lattice is stable under the divided powers of every integral multiple of a distinguished root vector.

source
theorem TauCeti.UniversalEnvelopingAlgebra.commute_kostantRootSubgroupPoints {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j : ι} (hij : ⁅e i, e j⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (f g : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) :
Commute ((kostantRootSubgroupPoints e h ρ M hM i hi) f) ((kostantRootSubgroupPoints e h ρ M hM j hj) g)

The degenerate Chevalley commutator relation for Kostant root subgroups. Root subgroups attached to commuting root vectors commute. For a root system this is the case of two roots whose sum is not a root and which are not opposite.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_mul_of_lie_eq {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k : ι} {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (f g w : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (hw : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv w) = ↑c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) :
(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) w * (kostantRootSubgroupPoints e h ρ M hM i hi) f

The Chevalley commutator relation for Kostant root subgroups. Suppose the distinguished root vectors satisfy ⁅eᵢ, eⱼ⁆ = c • eₖ with eₖ central for both, and let w be any 𝔾ₐ-point whose parameter is c times the product of the parameters of f and g. Then

xᵢ(f) xⱼ(g) = xⱼ(g) xₖ(w) xᵢ(f).

The hypotheses are exactly the class-two case of the Chevalley commutator formula: α + β is a root, while 2α + β and α + 2β are not.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_mul_of_lie_eq' {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k : ι} {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (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 * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))))) * (kostantRootSubgroupPoints e h ρ M hM i hi) f

The Chevalley commutator relation with the third 𝔾ₐ-point written out: it is the point whose parameter is c times the product of the parameters of f and g.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_conj_of_lie_eq {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k : ι} {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (f g w : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (hw : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv w) = ↑c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) :
(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) w

The conjugation form of the Chevalley commutator relation: conjugating the root subgroup of eⱼ by the root subgroup of eᵢ multiplies it by the root subgroup of eₖ, at the parameter c * t * u.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_conj_of_lie_eq' {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k : ι} {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (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 i hi) f)⁻¹ = (kostantRootSubgroupPoints e h ρ M hM j hj) g * (kostantRootSubgroupPoints e h ρ M hM k hk) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g)))))

The conjugation form of the Chevalley commutator relation with the third 𝔾ₐ-point written out: it is the point whose parameter is c times the product of the parameters of f and g.

source
theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupPoints_of_lie_eq {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k : ι} {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (f g z : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) (hz : Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv z) = ↑c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))) :
⁅(kostantRootSubgroupPoints e h ρ M hM i hi) f, (kostantRootSubgroupPoints e h ρ M hM j hj) g⁆ = (kostantRootSubgroupPoints e h ρ M hM k hk) z

The canonical class-two Chevalley commutator relation for Kostant root-subgroup actions. Suppose ⁅eᵢ, eⱼ⁆ = c • eₖ, with eₖ commuting with eᵢ and eⱼ, and let z have additive parameter c times the product of the parameters of f and g. Then ⁅xᵢ(f), xⱼ(g)⁆ = xₖ(z).

source
theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupPoints_of_lie_eq' {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k : ι} {c : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hik : ⁅e i, e k⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (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 k hk) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g)))))

The canonical class-two Chevalley commutator relation with the third 𝔾ₐ-point written out at parameter c times the product of the parameters of f and g.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_mul_of_lie_lie_eq {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k l : ι} {c d : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hiij : ⁅e i, ⁅e i, e j⁆⁆ = (2 * d) • e l) (hil : ⁅e i, e l⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hkl : ⁅e k, e l⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (hl : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e l)))) (f g p q : 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))) :
(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 i hi) f

The Chevalley commutator relation for Kostant root subgroups along the chain β, α + β, 2α + β. Suppose the distinguished root vectors satisfy

⁅eᵢ, eⱼ⁆ = c • eₖ,   ⁅eᵢ, ⁅eᵢ, eⱼ⁆⁆ = (2 * d) • e_l,

with ⁅eᵢ, e_l⁆ = ⁅eⱼ, eₖ⁆ = ⁅eₖ, e_l⁆ = 0, and let p, q be 𝔾ₐ-points whose parameters are c t u and d t² u, where t and u are the parameters of f and g. Then

xᵢ(f) xⱼ(g) = xⱼ(g) xₖ(p) x_l(q) xᵢ(f).

These hypotheses are the case of the Chevalley commutator formula in which the roots i α + j β with i, j > 0 are exactly α + β and 2 α + β; the factor 2 in the second bracket records that the integral element of the Kostant form is (ad eᵢ)² eⱼ / 2.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_mul_of_lie_lie_eq' {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k l : ι} {c d : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hiij : ⁅e i, ⁅e i, e j⁆⁆ = (2 * d) • e l) (hil : ⁅e i, e l⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hkl : ⁅e k, e l⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (hl : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e l)))) (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 * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))))) * (kostantRootSubgroupPoints e h ρ M hM l hl) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑d * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 2 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))))) * (kostantRootSubgroupPoints e h ρ M hM i hi) f

The Chevalley commutator relation for the chain β, α + β, 2α + β, with the two extra 𝔾ₐ-points written out: their parameters are c t u and d t² u.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_conj_of_lie_lie_eq {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k l : ι} {c d : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hiij : ⁅e i, ⁅e i, e j⁆⁆ = (2 * d) • e l) (hil : ⁅e i, e l⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hkl : ⁅e k, e l⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (hl : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e l)))) (f g p q : 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))) :
(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

The conjugation form of the Chevalley commutator relation for the chain β, α + β, 2α + β: conjugating the root subgroup of eⱼ by that of eᵢ multiplies it by the root subgroups of eₖ and of e_l, at the parameters c t u and d t² u.

source
theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPoints_conj_of_lie_lie_eq' {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) {A : Type u_2} [CommRing A] [Algebra ℤ A] {i j k l : ι} {c d : ℤ} (hij : ⁅e i, e j⁆ = c • e k) (hiij : ⁅e i, ⁅e i, e j⁆⁆ = (2 * d) • e l) (hil : ⁅e i, e l⁆ = 0) (hjk : ⁅e j, e k⁆ = 0) (hkl : ⁅e k, e l⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (hl : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e l)))) (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 i hi) f)⁻¹ = (kostantRootSubgroupPoints e h ρ M hM j hj) g * (kostantRootSubgroupPoints e h ρ M hM k hk) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑c * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g))))) * (kostantRootSubgroupPoints e h ρ M hM l hl) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd (↑d * (Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv f) ^ 2 * Multiplicative.toAdd (AdditiveGroup.gaPointsMulEquiv g)))))

The conjugation form of the Chevalley commutator relation for the chain β, α + β, 2α + β, with the two extra 𝔾ₐ-points written out.