When the Kostant weight torus is scheme-theoretically redundant

The Kostant toral closure is defined by adjoining a represented weight torus to a family of represented root subgroups. This file proves that the torus may be removed from the scheme-theoretic generating family whenever its universal point is already contained in the elementary subgroup generated by the root subgroups.

Under this universal-point hypothesis, the root-generated and toral defining ideals and affine group schemes are equal, and the canonical comparison between the carriers is an isomorphism. These results are integral and require no reducedness or finite-type hypothesis. The equality of defining ideals persists in the transported general-linear presentations over every commutative ring; this does not identify the transported carrier with the subgroup generated anew over a non-flat base.

The same hypothesis also removes the weight-torus hypothesis from rigidity: a homomorphism out of the toral carrier is then determined by its restrictions to the root subgroups alone, which is the uniqueness statement a consumer pinning an endomorphism by its action on the numbered simple root subgroups needs.

Main results

• kostantToralDefiningIdeal_eq_kostantGeneratedDefiningIdeal_of_universal_torus_mem_elementary: generation of the represented universal torus point implies equality of the two defining Hopf ideals.
• kostantToralGroupScheme_eq_kostantGeneratedGroupScheme_of_universal_torus_mem_elementary: under the same hypothesis, the root-generated and toral carriers are equal.
• kostantGeneratedToToral_eq_eqToHom_of_universal_torus_mem_elementary: the canonical comparison is the transport along that equality, and hence is an isomorphism.
• kostantToralBaseChangePresentationIdeal_eq_generated_of_universal_torus_mem_elementary: under the same hypothesis, the transported toral and root-generated presentations agree over every commutative ring.
• kostantToralGroupScheme_hom_ext_of_universal_torus_mem_elementary: under the same hypothesis, homomorphisms out of the toral carrier are determined by the root subgroups alone.

References

• R. Steinberg, Lectures on Chevalley Groups, Section 3.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 1.4.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedDefiningIdeal_toIdeal_le_torus_ker_of_universal_torus_mem_elementary {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (kostantTorusPoints M b wt ↑A) (SplitTorus.pointsMulEquiv q) ∈ kostantElementarySubgroup e h ρ M hM hnil A) : (kostantGeneratedDefiningIdeal e h ρ M hM hnil b).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap wt))).toRingHom

If the represented universal weight-torus point belongs to the elementary subgroup, then the root-generated defining ideal is killed by the weight-torus coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralDefiningIdeal_eq_kostantGeneratedDefiningIdeal_of_universal_torus_mem_elementary {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (kostantTorusPoints M b wt ↑A) (SplitTorus.pointsMulEquiv q) ∈ kostantElementarySubgroup e h ρ M hM hnil A) : kostantToralDefiningIdeal e h ρ M hM hnil b wt = kostantGeneratedDefiningIdeal e h ρ M hM hnil b

A root-generated universal weight-torus point makes the torus scheme-theoretically redundant. If the represented torus over its own coordinate ring belongs to the elementary subgroup, then adjoining the torus does not change the common-kernel defining Hopf ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_eq_kostantGeneratedGroupScheme_of_universal_torus_mem_elementary {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (kostantTorusPoints M b wt ↑A) (SplitTorus.pointsMulEquiv q) ∈ kostantElementarySubgroup e h ρ M hM hnil A) : kostantToralGroupScheme e h ρ M hM hnil b wt = kostantGeneratedGroupScheme e h ρ M hM hnil b

When the universal weight-torus point is generated by the root subgroups, the root-generated Kostant carrier and the toral closure are the same affine group scheme.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedToToral_eq_eqToHom_of_universal_torus_mem_elementary {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (kostantTorusPoints M b wt ↑A) (SplitTorus.pointsMulEquiv q) ∈ kostantElementarySubgroup e h ρ M hM hnil A) : kostantGeneratedToToral e h ρ M hM hnil b wt = CategoryTheory.eqToHom ⋯

Under generation of the universal torus point, the canonical inclusion of the root-generated carrier into the toral closure is the transport along their equality.

theorem TauCeti.UniversalEnvelopingAlgebra.isIso_kostantGeneratedToToral_of_universal_torus_mem_elementary {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (kostantTorusPoints M b wt ↑A) (SplitTorus.pointsMulEquiv q) ∈ kostantElementarySubgroup e h ρ M hM hnil A) : CategoryTheory.IsIso (kostantGeneratedToToral e h ρ M hM hnil b wt)

Generation of the universal weight-torus point makes the canonical comparison from the root-generated carrier to the toral closure an isomorphism.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal_eq_generated_of_universal_torus_mem_elementary {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (kostantTorusPoints M b wt ↑A) (SplitTorus.pointsMulEquiv q) ∈ kostantElementarySubgroup e h ρ M hM hnil A) (A : Type u_1) [CommRing A] : kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A = kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A

Generation of the universal weight-torus point makes the transported toral and root-generated presentations in O(GLₙ/A) equal, for every commutative ring A. This does not identify them with the common kernel of the root-subgroup maps formed anew over A.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_hom_ext_of_universal_torus_mem_elementary {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (huniv : let T := (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj; let A := ↧↑T; have q := WithConv.toConv (AlgHom.id ℤ ↑T); (kostantTorusPoints M b wt ↑A) (SplitTorus.pointsMulEquiv q) ∈ kostantElementarySubgroup e h ρ M hM hnil A) {Y : CommHopfAlgCat ℤ} (φ ψ : kostantToralGroupScheme e h ρ M hM hnil b wt ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : I), CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) φ = CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) ψ) : φ = ψ

A root-generated weight torus makes the torus hypothesis of rigidity redundant. If the represented universal weight-torus point belongs to the elementary subgroup, then two homomorphisms out of the toral carrier are equal as soon as they agree on every represented root subgroup, with no hypothesis on the weight torus. Compare kostantToralGroupScheme_hom_ext, where the torus restriction is a second hypothesis because the torus is in general an independent generator.