The Gβ short-pair relation on represented Kostant root subgroups #
The represented morphisms xα΅’ : πΎβ βΆ GLβ satisfy the Gβ short-pair product relation
on points over every commutative ring. The three additional factors have parameters
2ctu, 3dtΒ²u, and 3atuΒ², for the scaled brackets specified below. No structure
constant or factorial is inverted in the parameter ring.
This is the represented scheme-point form of
kostantRootSubgroupPoints_mul_of_g2_short_pair. It supplies the same relation inside
the closed group scheme generated by the root subgroups.
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.schemePointsMulEquiv_kostantRootSubgroup_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 : β 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 : 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)
(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 : (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))
:
(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 f (kostantRootSubgroup e h Ο M hM i hi basis).hom.hom)
The Gβ short-pair product relation for scheme-valued points of the represented Kostant
root subgroups, at the three additional parameters 2ctu, 3dtΒ²u, and 3atuΒ².
theorem
TauCeti.UniversalEnvelopingAlgebra.schemePointsMulEquiv_kostantRootSubgroup_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 : β 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 : 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)
(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 : (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 * (2 * 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 * (3 * 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 * (3 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) f) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) g) ^ 2))))
(kostantRootSubgroup e h Ο M hM m hm basis).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A)
(CategoryTheory.CategoryStruct.comp f (kostantRootSubgroup e h Ο M hM i hi basis).hom.hom)
The Gβ short-pair product relation on represented scheme points, with the three output
points written explicitly at parameters 2ctu, 3dtΒ²u, and 3atuΒ².