Points of the group scheme generated by Kostant root subgroups

The closed group scheme kostantGeneratedGroupScheme is defined by the largest Hopf ideal killed by every represented Kostant root subgroup. Its algebra-valued points therefore contain every root subgroup point. This file transports that fact through the general-linear point equivalence and proves that they contain the existing pointwise elementary group generated by those root subgroups.

Only this formal inclusion is asserted. Identifying the two groups of points over an algebraically closed field is the converse direction and requires a genuine generation theorem for the chosen Chevalley--Demazure group; it does not follow from the common-kernel universal property.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedPointsSubgroup: the algebra-valued points of the generated closed group scheme, viewed as matrices in GLₙ.
• TauCeti.UniversalEnvelopingAlgebra.mem_kostantGeneratedPointsSubgroup_iff: membership in those points is vanishing of the associated convolution point on the defining Hopf ideal.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_mem_generatedPoints: every represented root-subgroup matrix is a point of the generated group scheme.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_le_of_matrix_mem: in basis coordinates the elementary group lies in any subgroup of GLₙ containing all represented root-subgroup matrices.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_le_generatedPoints: the pointwise elementary group, in basis coordinates, lies in the generated group-scheme points.

This advances the "points over an algebraically closed field" and Chevalley--Demazure construction targets in Layer 9 of the ReductiveGroups roadmap. The resulting point group is an input to the pinned ambient groups in milestone L0 of the CFSGStatement roadmap.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedPointsSubgroup {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, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type v) [CommRing A] : Subgroup (GL (Fin n) A)

The algebra-valued points of the closed group scheme generated by the represented Kostant root subgroups, embedded in GLₙ using its quotient presentation and the basis b.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedPointsSubgroup_def {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, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type v) [CommRing A] : kostantGeneratedPointsSubgroup e h ρ M hM hnil b A = GeneralLinear.hopfIdealPointsSubgroup n (kostantGeneratedDefiningIdeal e h ρ M hM hnil b) A

The generated group-scheme points are the general-linear point subgroup cut out by the generated defining Hopf ideal.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantGeneratedPointsSubgroup_iff {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, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type v) [CommRing A] (g : GL (Fin n) A) : g ∈ kostantGeneratedPointsSubgroup e h ρ M hM hnil b A ↔ ∀ x ∈ kostantGeneratedDefiningIdeal e h ρ M hM hnil b, ((GeneralLinear.pointsMulEquiv n).symm g).ofConv x = 0

Membership in the points of the generated closed group scheme is vanishing on its defining Hopf ideal: a matrix of GLₙ is such a point exactly when the convolution point it corresponds to under GeneralLinear.pointsMulEquiv kills kostantGeneratedDefiningIdeal.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix_mem_generatedPoints {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, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type v) [CommRing A] (i : I) (q : ↑(HopfAlgebra.points ↧A)) : (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q ∈ kostantGeneratedPointsSubgroup e h ρ M hM hnil b A

Every represented Kostant root-subgroup matrix belongs to the algebra-valued points of the closed group scheme generated by all the root subgroups.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_le_of_matrix_mem {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, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type v) [CommRing A] {H : Subgroup (GL (Fin n) A)} (hH : ∀ (i : I) (q : ↑(HopfAlgebra.points ↧A)), (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q ∈ H) : Subgroup.map (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv) (kostantElementarySubgroup e h ρ M hM hnil ↧A) ≤ H

The generation criterion for the pointwise Kostant elementary group. In basis coordinates the elementary group is generated by the represented root-subgroup matrices, so it lies in any subgroup of GLₙ containing all of them.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantElementarySubgroup_le_generatedPoints {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, ∀ m ∈ M, (ρ u) m ∈ M) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type v) [CommRing A] : Subgroup.map (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv) (kostantElementarySubgroup e h ρ M hM hnil ↧A) ≤ kostantGeneratedPointsSubgroup e h ρ M hM hnil b A

The pointwise Kostant elementary group, after writing its automorphisms in the basis b, is contained in the algebra-valued points of the closed group scheme generated by the same root subgroups.