Kostant root subgroups inside the generated group scheme

The group scheme generated by a family of represented Kostant root subgroups comes with a factorization of each map xᵢ : 𝔾ₐ ⟶ GLₙ through the generated carrier. A pinning needs the stronger statement that this factored map is still a closed immersion, so that it presents a closed copy of 𝔾ₐ inside the generated group rather than only a morphism into it.

Under the root-step hypotheses used to prove that xᵢ : 𝔾ₐ ⟶ GLₙ is a closed immersion, its coordinate map is surjective. The coordinate map after factorization through the common-kernel quotient is therefore also surjective: its composite with the quotient map is the original coordinate map. The affine closed-immersion criterion then gives the desired result directly.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupGeneratedCoordinateMap_surjective: the factored coordinate map remains surjective.
• TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantRootSubgroupToGenerated: the factored root-subgroup morphism is a closed immersion.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupInGenerated: the resulting closed subgroup scheme of the generated Chevalley carrier.

References

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" milestones in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupGeneratedCoordinateMap_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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {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 (kostantRootSubgroupGeneratedCoordinateMap e h ρ M hM hnil b i))

The coordinate map of a Kostant root subgroup remains surjective after it is factored through the coordinate ring of the generated group scheme.

theorem TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {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 (kostantRootSubgroupToGenerated e h ρ M hM hnil b i).hom.hom)

The ith Kostant root subgroup is a closed immersion into the group scheme generated by all the represented root subgroups. Thus the factorization through the generated carrier presents a closed copy of 𝔾ₐ, as required by the root-subgroup data of a pinning.

theorem TauCeti.UniversalEnvelopingAlgebra.mono_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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {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 (kostantRootSubgroupToGenerated e h ρ M hM hnil b i)

A factored Kostant root subgroup is a monomorphism into the generated group scheme.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupInGenerated {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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {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 (kostantGeneratedGroupScheme e h ρ M hM hnil b)

The ith Kostant root subgroup as a closed subgroup scheme of the generated Chevalley carrier. Its representing arrow is the factorization of xᵢ through that carrier.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantRootSubgroupInGenerated {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) (i : I) (hnil : ∀ (j : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) {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) : ↑(kostantRootSubgroupInGenerated e h ρ M hM i hnil b hc hstep hsq) = CategoryTheory.Subobject.mk (kostantRootSubgroupToGenerated e h ρ M hM hnil b i)

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