The toral Kostant carrier inside a constant-multiplication subgroup scheme

Fix a bilinear multiplication on ℤⁿ given by constant structure matrices C : Fin n → Matrix (Fin n) (Fin n) ℤ, and let TauCeti.ConstantMultiplication.definingHopfIdeal be the Hopf ideal cutting out the subgroup scheme of GLₙ whose points are the invertible matrices multiplicative for that product.

The toral Kostant carrier is the smallest closed subgroup scheme of GLₙ containing the represented root subgroups and the represented weight torus, so it lies inside that subgroup scheme as soon as its generators do. Since the defining ideal of the carrier is the largest Hopf ideal killed by the root-subgroup and weight-torus coordinate maps, the containment of Hopf ideals reduces to evaluating the defining relations on the generic matrix of each generating coordinate map — equivalently, to checking multiplicativity of the divided-power exponential matrices and of the weight-diagonal matrices over every commutative ring. On points this says that every matrix point of the carrier is multiplicative for the product.

Only the containment is proved. Nothing here asserts that the carrier exhausts the points of the constant-multiplication subgroup scheme, or that either group scheme is reductive or smooth.

Main results

In the namespace TauCeti.UniversalEnvelopingAlgebra:

• constantMultiplicationDefiningHopfIdeal_le_kostantToralDefiningIdeal and preserves_of_mem_kostantToralPointsSubgroup: the containment of Hopf ideals and its consequence on matrix points, from the generic matrices of the generating coordinate maps.
• constantMultiplicationDefiningHopfIdeal_le_kostantToralDefiningIdeal_of_generators and preserves_of_mem_kostantToralPointsSubgroup_of_generators: the same two statements from multiplicativity of the generator matrices over every commutative ring.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1, for the torus and root subgroups generating the Chevalley group.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.

The reduction of a containment of Hopf ideals to the generating coordinate maps is the one carried out for a constant bilinear form in TauCeti.SpStd; the statements below package it once for an arbitrary constant multiplication and an arbitrary toral Kostant carrier.

theorem TauCeti.UniversalEnvelopingAlgebra.constantMultiplicationDefiningHopfIdeal_le_kostantToralDefiningIdeal {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (C : Fin n → Matrix (Fin n) (Fin n) ℤ) (hroot : ∀ (i : I), ConstantMultiplication.Preserves ℤ n C ((GeneralLinear.genericMatrix ℤ n).map ⇑↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)))) (htorus : ConstantMultiplication.Preserves ℤ n C ((GeneralLinear.genericMatrix ℤ n).map ⇑↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap wt)))) : ConstantMultiplication.definingHopfIdeal ℤ n C ≤ kostantToralDefiningIdeal e h ρ M hM hnil b wt

The generators of the toral Kostant carrier cut out the multiplication. If the generic matrix of every represented root-subgroup coordinate map and of the represented weight-torus coordinate map preserves the multiplication with structure matrices C, then the Hopf ideal cutting out the subgroup scheme preserving that multiplication is contained in the toral defining ideal. Equivalently, the toral carrier is a closed subgroup scheme of the group scheme preserving the multiplication.

theorem TauCeti.UniversalEnvelopingAlgebra.preserves_of_mem_kostantToralPointsSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (C : Fin n → Matrix (Fin n) (Fin n) ℤ) (hroot : ∀ (i : I), ConstantMultiplication.Preserves ℤ n C ((GeneralLinear.genericMatrix ℤ n).map ⇑↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)))) (htorus : ConstantMultiplication.Preserves ℤ n C ((GeneralLinear.genericMatrix ℤ n).map ⇑↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap wt)))) (A : Type v) [CommRing A] {g : GL (Fin n) A} (hg : g ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) : ConstantMultiplication.Preserves ℤ n C ↑g

Every matrix point of the toral Kostant carrier preserves the multiplication, as soon as the generic matrices of the root-subgroup and weight-torus coordinate maps do.

The criterion on the generator matrices

theorem TauCeti.UniversalEnvelopingAlgebra.constantMultiplicationDefiningHopfIdeal_le_kostantToralDefiningIdeal_of_generators {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (C : Fin n → Matrix (Fin n) (Fin n) ℤ) (hroot : ∀ (i : I) (A : Type) [inst : CommRing A] (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), ConstantMultiplication.Preserves ℤ n C ↑((kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q)) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), ConstantMultiplication.Preserves ℤ n C ↑((kostantTorusMatrix M b wt) s)) : ConstantMultiplication.definingHopfIdeal ℤ n C ≤ kostantToralDefiningIdeal e h ρ M hM hnil b wt

The toral Kostant carrier preserves a multiplication preserved by its generators. If every represented root-subgroup matrix and every represented weight-torus matrix preserves the multiplication with structure matrices C, over every commutative ring, then the Hopf ideal cutting out the subgroup scheme preserving that multiplication is contained in the toral defining ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.preserves_of_mem_kostantToralPointsSubgroup_of_generators {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Finite κ] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (C : Fin n → Matrix (Fin n) (Fin n) ℤ) (hroot : ∀ (i : I) (A : Type) [inst : CommRing A] (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), ConstantMultiplication.Preserves ℤ n C ↑((kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q)) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), ConstantMultiplication.Preserves ℤ n C ↑((kostantTorusMatrix M b wt) s)) (A : Type v) [CommRing A] {g : GL (Fin n) A} (hg : g ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) : ConstantMultiplication.Preserves ℤ n C ↑g

Every matrix point of the toral Kostant carrier preserves a multiplication preserved by its generators.