Chevalley relations for Kostant root-subgroup scheme morphisms

The divided-power construction represents a root action by an affine group-scheme morphism 𝔾ₐ → GLₙ. This file proves the commuting and class-two Chevalley relations on the scheme-valued points of those actual morphisms. It transports the universe-polymorphic matrix relations from ChevalleyRelations.lean through the point comparison proved in Scheme/Basic.lean. The longer exceptional relation is developed separately in Scheme/Relations/G2/Basic.lean.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.commute_schemePointsMulEquiv_kostantRootSubgroup: commuting root vectors give commuting scheme-valued root-subgroup points.
• TauCeti.UniversalEnvelopingAlgebra. commutatorElement_schemePointsMulEquiv_kostantRootSubgroup_of_lie_eq: the class-two Chevalley commutator relation for scheme-valued points.
• TauCeti.UniversalEnvelopingAlgebra. commutatorElement_schemePointsMulEquiv_kostantRootSubgroup_of_lie_eq': the same relation with the third scheme-valued point written out.

The representation carrier is universe-zero because the current group-scheme reconstruction API requires the base, coordinate Hopf algebra, and comodule to inhabit the same universe.

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_schemePointsMulEquiv_kostantRootSubgroup {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 : I} (hij : ⁅e i, e j⁆ = 0) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (AdditiveGroup.groupScheme ℤ).X) : Commute ((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))

Scheme-valued points of represented Kostant root subgroups attached to commuting root vectors commute.

theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_schemePointsMulEquiv_kostantRootSubgroup_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) (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) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (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))) : ⁅(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)

The class-two Chevalley commutator relation on scheme-valued points of represented Kostant root subgroups. Suppose ⁅eᵢ, eⱼ⁆ = c • eₖ, with eₖ commuting with eᵢ and eⱼ, and let r have additive parameter c times the product of the parameters of p and q. Then the matrix commutator of the represented i- and j-root values is the represented k-root value at r.

theorem TauCeti.UniversalEnvelopingAlgebra.commutatorElement_schemePointsMulEquiv_kostantRootSubgroup_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) (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) (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) (hk : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (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)

The class-two Chevalley commutator relation on scheme-valued points with the third point written out at parameter c times the product of the parameters of p and q.