The group scheme generated by Kostant root subgroups

Fix a finite free Kostant-stable lattice with basis b. Every distinguished nilpotent root vector gives a represented root-subgroup morphism xᵢ : 𝔾ₐ ⟶ GLₙ. This file constructs the smallest closed subgroup scheme of GLₙ containing all of those morphisms.

On coordinate Hopf algebras, its defining ideal is the largest Hopf ideal contained in the kernel of every root-subgroup coordinate map. Quotienting by that ideal therefore gives an explicit affine group scheme, and every xᵢ factors through it. The universal property proves minimality among closed subgroup schemes of GLₙ presented by Hopf-ideal quotients.

This is the scheme-level counterpart of kostantElementarySubgroup, the subgroup generated on points. Identifying its points over an algebraically closed field with that elementary subgroup is a later theorem and is not asserted here.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal: the common-kernel Hopf ideal, with kostantGeneratedDefiningIdeal_def exposing its defining equation to downstream modules.
• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme: the resulting closed subgroup scheme of GLₙ.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated: the factorization of every root subgroup through the generated group scheme.
• kostantRootSubgroupGeneratedCoordinateMap_surjective_of_surjective: a surjective root-subgroup coordinate map stays surjective after factorization.
• TauCeti.UniversalEnvelopingAlgebra.le_kostantGeneratedDefiningIdeal_iff: the minimality universal property in coordinate form.

References

The construction is the scheme-theoretic subgroup generated by the root subgroups in the Chevalley--Demazure construction; see J. E. Humphreys, Linear Algebraic Groups, §26, and R. W. Carter, Simple Groups of Lie Type, §4.4. It advances Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md and supplies the explicit ambient carrier required by milestone L0 of the CFSGStatement roadmap.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal {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) : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)

The defining Hopf ideal of the closed subgroup scheme generated by all represented Kostant root subgroups. It is the largest Hopf ideal killed by every root-subgroup coordinate map.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal_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) : kostantGeneratedDefiningIdeal e h ρ M hM hnil b = CommHopfAlgCat.commonKernelHopfIdeal fun (i : I) => kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b

The defining ideal of the generated group scheme is the common-kernel Hopf ideal of its root subgroup coordinate maps.

theorem TauCeti.UniversalEnvelopingAlgebra.le_kostantGeneratedDefiningIdeal_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) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) : J ≤ kostantGeneratedDefiningIdeal e h ρ M hM hnil b ↔ ∀ (i : I), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b))).toRingHom

A Hopf ideal is contained in the defining ideal of the generated group scheme exactly when every Kostant root-subgroup coordinate map kills it. This is the coordinate form of minimality.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal_toIdeal_le_ker {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) (i : I) : (kostantGeneratedDefiningIdeal e h ρ M hM hnil b).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b))).toRingHom

Every root-subgroup coordinate map kills the defining ideal of the generated group scheme.

@[reducible, inline]

noncomputable abbrev TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGroupScheme {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) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The affine group scheme generated by the represented Kostant root subgroups: the Hopf spectrum of the general-linear coordinate algebra modulo their common-kernel Hopf ideal.

Equations

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGroupSchemeι {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) : kostantGeneratedGroupScheme e h ρ M hM hnil b ⟶ GeneralLinear.groupScheme ℤ n

The generated group scheme is a closed subgroup scheme of GLₙ.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGroupSchemeι_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) : kostantGeneratedGroupSchemeι e h ρ M hM hnil b = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantGeneratedDefiningIdeal e h ρ M hM hnil b)) (CategoryTheory.eqToHom ⋯)

The inclusion of the generated group scheme is the quotient-spectrum inclusion, transported across the named presentation of GLₙ.

instance TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantGeneratedGroupSchemeι {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) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantGeneratedGroupSchemeι e h ρ M hM hnil b).hom.hom)

The inclusion of the generated group scheme into GLₙ is a closed immersion.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupGeneratedCoordinateMap {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) (i : I) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantGeneratedDefiningIdeal e h ρ M hM hnil b) ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The coordinate map from the generated-group quotient to the additive-group coordinate ring through which the ith root subgroup factors.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantRootSubgroupGeneratedCoordinateMap {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) (i : I) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantGeneratedDefiningIdeal e h ρ M hM hnil b)) (kostantRootSubgroupGeneratedCoordinateMap e h ρ M hM hnil b i) = kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b

Composing the quotient morphism with the ith generated coordinate map recovers the ith root-subgroup coordinate map. This characterizes the generated coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupGeneratedCoordinateMap_surjective_of_surjective {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) (i : I) (hi : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b))) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupGeneratedCoordinateMap e h ρ M hM hnil b i))

If a root-subgroup coordinate map is surjective before factorization through the generated coordinate ring, then the factored coordinate map is also surjective.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated {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) (i : I) : AdditiveGroup.groupScheme ℤ ⟶ kostantGeneratedGroupScheme e h ρ M hM hnil b

The ith Kostant root subgroup, factored through the generated group scheme.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_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) (i : I) : kostantRootSubgroupToGenerated e h ρ M hM hnil b i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.hopfSpec ↧ℤ).map (kostantRootSubgroupGeneratedCoordinateMap e h ρ M hM hnil b i).op)

The factored root subgroup is relative spectrum applied to its quotient coordinate map, transported across the named presentation of 𝔾ₐ.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_comp_ι {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) (i : I) : CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToGenerated e h ρ M hM hnil b i) (kostantGeneratedGroupSchemeι e h ρ M hM hnil b) = kostantRootSubgroup e h ρ M hM i ⋯ b

Factoring a root subgroup through the generated group scheme and then including into GLₙ recovers the original represented root-subgroup morphism.