Multiply-laced Chevalley relations for Kostant root-subgroup scheme morphisms

This file transports a conditional multiply-laced Chevalley commutator relation to scheme-valued points of the represented root-subgroup morphisms xᵢ : 𝔾ₐ → GLₙ. Under the stated bracket and nilpotence hypotheses for the chain β, α + β, 2α + β, the relation is

⁅x_α(t), x_β(u)⁆ = x_{α+β}(c t u) x_{2α+β}(d t² u).

It transports the matrix relation from RootSubgroup/MultiplyLacedRelations.lean through the point-comparison theorem for the actual affine group-scheme morphisms. Thus the equation is stated at the same interface used by the generated Chevalley--Demazure carrier.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra. commutatorElement_schemePointsMulEquiv_kostantRootSubgroup_of_lie_lie_eq: the multiply-laced relation for scheme-valued points.
• TauCeti.UniversalEnvelopingAlgebra. commutatorElement_schemePointsMulEquiv_kostantRootSubgroup_of_lie_lie_eq': the same relation with both output points written out.

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.commutatorElement_schemePointsMulEquiv_kostantRootSubgroup_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) (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) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (hl : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e l)))) (p q r s : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of ℤ)) ⟶ (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))) : ⁅(GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (kostantRootSubgroup e h ρ M hM i hi b).hom.hom), (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp q (kostantRootSubgroup e h ρ M hM j hj b).hom.hom)⁆ = (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp r (kostantRootSubgroup e h ρ M hM k hk b).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp s (kostantRootSubgroup e h ρ M hM l hl b).hom.hom)

The multiply-laced Chevalley commutator relation on scheme-valued points. Suppose the distinguished root vectors form the chain β, α + β, 2α + β, and let r and s carry parameters c t u and d t² u. Then the commutator of the represented i- and j-root values is the product of the represented k- and l-root values.

theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_schemePointsMulEquiv_kostantRootSubgroup_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) (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) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (hl : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e l)))) (p q : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of ℤ)) ⟶ (AdditiveGroup.groupScheme ℤ).X) : ⁅(GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp p (kostantRootSubgroup e h ρ M hM i hi b).hom.hom), (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp q (kostantRootSubgroup e h ρ M hM j hj b).hom.hom)⁆ = (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑c * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q))))) (kostantRootSubgroup e h ρ M hM k hk b).hom.hom) * (GeneralLinear.schemePointsMulEquiv n A) (CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑d * (Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) p) ^ 2 * Multiplicative.toAdd ((AdditiveGroup.schemePointsMulEquiv A) q))))) (kostantRootSubgroup e h ρ M hM l hl b).hom.hom)

The multiply-laced Chevalley commutator relation on scheme-valued points with both output points written out at parameters c t u and d t² u.