Chevalley relations in the generated Kostant group scheme #
The represented Kostant root subgroups factor through the closed group scheme they generate.
This file proves that the factored root subgroups satisfy their Chevalley relations intrinsically
in that generated carrier. The earlier matrix and scheme-point relations only identify the
images of these points in GLₙ; the closed immersion of the generated group scheme makes the
map on points injective, so those identities descend uniquely.
The results are stated on points over every commutative ring A : Type. Commuting root vectors
give commuting generated-group points, while a class-two root string
⁅eᵢ, eⱼ⁆ = c • eₖ gives
[xᵢ(s), xⱼ(t)] = xₖ(cst).
The file also transports the multiply-laced relation from
Scheme/MultiplyLacedRelations.lean and the type-G₂ relation from
Scheme/Relations/G2/Basic.lean, together with its short-pair counterpart in
Scheme/Relations/G2/ShortPair.lean. All these relations hold intrinsically on the
kostantRootSubgroupToGenerated interface.
Main declarations #
TauCeti.UniversalEnvelopingAlgebra.commute_kostantRootSubgroupToGenerated: commuting root vectors give commuting points of the generated group scheme.TauCeti.UniversalEnvelopingAlgebra. commutatorElement_kostantRootSubgroupToGenerated_of_lie_eq: the class-two Chevalley relation inside the generated group scheme.TauCeti.UniversalEnvelopingAlgebra. commutatorElement_kostantRootSubgroupToGenerated_of_lie_lie_eq: the multiply-laced Chevalley relation inside the generated group scheme.TauCeti.UniversalEnvelopingAlgebra. kostantRootSubgroupToGenerated_mul_of_lie_eq_three_nsmul: the type-G₂Chevalley relation inside the generated group scheme.
References #
- R. W. Carter, Simple Groups of Lie Type, Theorem 5.2.2.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Sections 26--27.
- J. C. Jantzen, Representations of Algebraic Groups, II.1.
theorem
TauCeti.UniversalEnvelopingAlgebra.commute_kostantRootSubgroupToGenerated
{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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(A : Type)
[CommRing A]
{i j : I}
(hij : ⁅e i, e j⁆ = 0)
(p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X)
:
Commute (CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom)
(CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom)
Represented Kostant root subgroups attached to commuting root vectors commute as points of the generated group scheme over every commutative value ring.
theorem
TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupToGenerated_of_lie_eq
{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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(A : Type)
[CommRing A]
{i j k : I}
{c : ℤ}
(hij : ⁅e i, e j⁆ = c • e k)
(hik : ⁅e i, e k⁆ = 0)
(hjk : ⁅e j, e k⁆ = 0)
(p q r : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X)
(hr :
Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) r) = ↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q)))
:
⁅CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom, CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom⁆ = CategoryTheory.CategoryStruct.comp r (kostantRootSubgroupToGenerated e h ρ M hM hnil b k).hom.hom
The class-two Chevalley commutator relation inside the generated Kostant group scheme.
Suppose ⁅eᵢ, eⱼ⁆ = c • eₖ, with eₖ commuting with both eᵢ and eⱼ. If the additive
parameter of r is c times the product of those of p and q, then the commutator of the
factored i- and j-root points is the factored k-root point at r.
@[simp]
theorem
TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupToGenerated_of_lie_eq'
{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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(A : Type)
[CommRing A]
{i j k : I}
{c : ℤ}
(hij : ⁅e i, e j⁆ = c • e k)
(hik : ⁅e i, e k⁆ = 0)
(hjk : ⁅e j, e k⁆ = 0)
(p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X)
:
⁅CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom, CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom⁆ = CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q)))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b k).hom.hom
The class-two Chevalley commutator relation inside the generated group scheme, with the
third point written explicitly at parameter c times the product of the first two parameters.
theorem
TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupToGenerated_of_lie_lie_eq
{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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(A : Type)
[CommRing A]
{i j k l : I}
{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)
(hjl : ⁅e j, e l⁆ = 0)
(hkl : ⁅e k, e l⁆ = 0)
(p q r s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X)
(hr :
Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) r) = ↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q)))
(hs :
Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) s) = ↑d * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q)))
:
⁅CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom, CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom⁆ = CategoryTheory.CategoryStruct.comp r (kostantRootSubgroupToGenerated e h ρ M hM hnil b k).hom.hom * CategoryTheory.CategoryStruct.comp s (kostantRootSubgroupToGenerated e h ρ M hM hnil b l).hom.hom
The multiply-laced Chevalley commutator relation inside the generated Kostant group
scheme. The indices i, j, k, l correspond to α, β, α + β, 2α + β. If r and s
have parameters c t u and d t² u, then the commutator of the factored i- and j-root
points is the product of the factored k- and l-root points.
theorem
TauCeti.UniversalEnvelopingAlgebra.commutatorElement_kostantRootSubgroupToGenerated_of_lie_lie_eq'
{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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(A : Type)
[CommRing A]
{i j k l : I}
{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)
(hjl : ⁅e j, e l⁆ = 0)
(hkl : ⁅e k, e l⁆ = 0)
(p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X)
:
⁅CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom, CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom⁆ = CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q)))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b k).hom.hom * CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑d * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q)))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b l).hom.hom
The multiply-laced Chevalley commutator relation inside the generated group scheme, with
both output points written explicitly at parameters c t u and d t² u.
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(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)
(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))
:
CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom * CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom = CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom * CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToGenerated e h ρ M hM hnil b k).hom.hom * CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToGenerated e h ρ M hM hnil b l).hom.hom * CategoryTheory.CategoryStruct.comp r (kostantRootSubgroupToGenerated e h ρ M hM hnil b m).hom.hom * CategoryTheory.CategoryStruct.comp s (kostantRootSubgroupToGenerated e h ρ M hM hnil b o).hom.hom * CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom
The type-G₂ Chevalley product relation inside the generated Kostant group scheme.
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.kostantRootSubgroupToGenerated_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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(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)
(f g : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X)
:
CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom * CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom = CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom * CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g)))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b k).hom.hom * CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑d * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g)))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b l).hom.hom * CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑a * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g)))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b m).hom.hom * CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑b' * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g) ^ 2))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b o).hom.hom * CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom
The type-G₂ Chevalley product relation inside the generated group scheme with the four
output points written explicitly at parameters c t u, d t² u, a t³ u, and b t³ u².
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_mul_of_g2_short_pair
{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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(A : Type)
[CommRing A]
{i j k l m : I}
{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)
(f g p q r : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X)
(hp :
Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) = ↑c * (2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g)))
(hq :
Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q) = ↑d * (3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g)))
(hr :
Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) r) = ↑a * (3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g) ^ 2))
:
CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom * CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom = CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom * CategoryTheory.CategoryStruct.comp p (kostantRootSubgroupToGenerated e h ρ M hM hnil b k).hom.hom * CategoryTheory.CategoryStruct.comp q (kostantRootSubgroupToGenerated e h ρ M hM hnil b l).hom.hom * CategoryTheory.CategoryStruct.comp r (kostantRootSubgroupToGenerated e h ρ M hM hnil b m).hom.hom * CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom
The G₂ short-pair relation inside the generated group scheme, with the output points
at parameters 2ctu, 3dt²u, and 3atu². The indices i, j, k, l, m correspond to
α, α + β, 2α + β, 3α + β, 3α + 2β.
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_mul_of_g2_short_pair'
{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 : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(A : Type)
[CommRing A]
{i j k l m : I}
{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)
(f g : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X)
:
CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom * CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom = CategoryTheory.CategoryStruct.comp g (kostantRootSubgroupToGenerated e h ρ M hM hnil b j).hom.hom * CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑c * (2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g)))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b k).hom.hom * CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑d * (3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g)))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b l).hom.hom * CategoryTheory.CategoryStruct.comp
((AdditiveGroup.schemePointsMulEquiv A).symm
(Multiplicative.ofAdd
(↑a * (3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g) ^ 2))))
(kostantRootSubgroupToGenerated e h ρ M hM hnil b m).hom.hom * CategoryTheory.CategoryStruct.comp f (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom
The G₂ short-pair product relation inside the generated group scheme, with the three output
points written explicitly at parameters 2ctu, 3dt²u, and 3atu².