The weight torus inside the Kostant toral closure

The Kostant toral closure is generated scheme-theoretically by represented root subgroups and a represented split torus. This file proves that, when the weights span the character lattice, the factored torus morphism into that closure is itself a closed immersion. It therefore packages the split torus as a closed subgroup scheme of the assembled carrier, rather than only as a morphism to it.

The proof compares the two existing constructions of the diagonal weight representation: the coordinate-map construction used by the toral closure and the comodule construction whose closed-immersion criterion is already available. Since the inclusion of the toral closure in GL_n is a closed immersion, closedness descends from their composite to the factored torus.

For Chevalley weight data this supplies the closed embedding needed toward constructing the torus component of a pinning on the assembled carrier. Identifying it as a maximal torus and constructing the compatible Borel remain part of Layer 9 of the ReductiveGroups roadmap, on the path to the ambient groups required by milestone L0 of the CFSGStatement roadmap.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantWeightTorusToToral: spanning weights make the factored weight torus a closed immersion.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusInToral: the corresponding closed subgroup scheme of the Kostant toral closure.

References

• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.

theorem TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantWeightTorusToToral {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 → κ → ℤ) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantWeightTorusToToral e h ρ M hM hnil b wt).hom.hom)

Spanning weights embed the represented split torus as a closed subgroup of the Kostant toral closure.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusInToral {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 → κ → ℤ) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : ClosedSubgroupScheme (kostantToralGroupScheme e h ρ M hM hnil b wt)

The split weight torus, with spanning weights, as a closed subgroup scheme of the Kostant toral closure.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantWeightTorusInToral {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 → κ → ℤ) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : have x := ⋯; ↑(kostantWeightTorusInToral e h ρ M hM hnil b wt hwt) = CategoryTheory.Subobject.mk (kostantWeightTorusToToral e h ρ M hM hnil b wt)

The underlying subobject of the closed weight torus in the toral closure is represented by the factored weight-torus morphism.