Kostant root subgroups inside the toral closure

The toral Kostant carrier is generated by represented root subgroups together with a represented weight torus. Each root-subgroup map factors through this carrier, but a pinning needs the stronger statement that the factored map is a closed immersion and hence presents a closed copy of 𝔾ₐ.

The usual root-step hypotheses make the original root-subgroup coordinate map surjective. Its factorization through the common-kernel quotient defining the toral carrier remains surjective, so the affine closed-immersion criterion applies. The resulting closed subgroup scheme is the root-subgroup datum used by a pinned Chevalley--Demazure carrier.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap_surjective: the factored coordinate map is surjective under the root-step hypotheses.
• TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantRootSubgroupToToral: the factored root-subgroup morphism is a closed immersion.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupInToral: the corresponding closed subgroup scheme of the toral carrier.

References

The declaration order, hypothesis layout, and proof organization adapt the existing formal template in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.RootInGenerated to the toral carrier.

The construction is the root-subgroup part of a pinning 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 the "Pinnings" and "Root subgroup maps" targets in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of the CFSGStatement roadmap.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap_surjective {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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupToralCoordinateMap e h ρ M hM hnil b wt i))

The coordinate map of a Kostant root subgroup remains surjective after factorization through the coordinate ring of the toral closure.

theorem TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantRootSubgroupToToral {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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantRootSubgroupToToral e h ρ M hM hnil b wt i).hom.hom)

The ith Kostant root subgroup is a closed immersion into the toral closure. Thus the factorization presents a closed copy of the additive group scheme in the carrier used by the pinned Chevalley--Demazure construction.

theorem TauCeti.UniversalEnvelopingAlgebra.mono_kostantRootSubgroupToToral {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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : CategoryTheory.Mono (kostantRootSubgroupToToral e h ρ M hM hnil b wt i)

A Kostant root subgroup factored through the toral closure is a monomorphism.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupInToral {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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : ClosedSubgroupScheme (kostantToralGroupScheme e h ρ M hM hnil b wt)

The ith Kostant root subgroup as a closed subgroup scheme of the toral closure. Its representing arrow is the factored root-subgroup morphism.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantRootSubgroupInToral {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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {r s : Fin n} {c : ℤ} (hc : IsUnit c) (hstep : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s) = c • ↑(b r)) (hsq : (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ↑(b s)) = 0) : ↑(kostantRootSubgroupInToral e h ρ M hM i hnil b wt hc hstep hsq) = CategoryTheory.Subobject.mk (kostantRootSubgroupToToral e h ρ M hM hnil b wt i)

The subobject underlying kostantRootSubgroupInToral is represented by the factored root-subgroup morphism itself.