Closed subschemes generated by a torus and selected Kostant root subgroups

Fix the data defining a Kostant toral closure inside GLₙ, and let S be a set of its root indices. This file constructs the smallest closed subgroup scheme of GLₙ containing the represented weight torus and the root-subgroup morphisms indexed by S. Its defining Hopf ideal is the largest one killed by those morphisms; concretely, it is the common-kernel Hopf ideal of the selected root-subgroup coordinate maps and the weight-torus coordinate map.

The resulting carrier is a closed subgroup scheme of the full toral closure. The inclusion is functorial in S, and both the selected root subgroups and the weight torus factor through it. For a positive system, this is the scheme-level candidate for the Borel component of a pinning. No maximal-solvability or reductivity statement is made here: proving that this closed carrier is a Borel subgroup for the Chevalley data is later geometric work.

This construction is the scheme counterpart of TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemSubgroup, which generates a subgroup on points. The pointwise subgroup maps into the points of this closed carrier, but equality can fail over a general value ring and is not asserted here.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal: the common-kernel Hopf ideal for the selected root subgroups and the weight torus.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupScheme: the corresponding closed subgroup scheme of GLₙ.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemToToral: its closed immersion into the full toral closure.
• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemClosedSubgroup_le_iff: its minimality among closed subgroups containing the selected root subgroups and weight torus.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToTorusSubsystem and TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToTorusSubsystem: the selected represented root-subgroup morphisms and the represented weight-torus morphism, factored through the subsystem carrier.

References

• J. E. Humphreys, Linear Algebraic Groups, §§26--28.
• R. W. Carter, Simple Groups of Lie Type, §§4.4, 8.2, and 8.5.

Formally, this file follows and reuses TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.ToralClosure.Basic, whose generator family, defining ideal and factorization pattern for the full toral closure it specializes to a selected set of root indices, and it is the scheme-level counterpart of the pointwise subsystem subgroups in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Borel.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)

The defining Hopf ideal of the closed subgroup scheme generated by the represented weight torus and the Kostant root subgroups indexed by S. It is the common-kernel Hopf ideal of the toral generator family restricted to S.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal_def {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS = CommHopfAlgCat.commonKernelHopfIdeal fun (j : ↑S ⊕ Unit) => match j with | Sum.inl i => kostantRootSubgroupCoordinateMap e h ρ M hM ↑i ⋯ b | Sum.inr val => GeneralLinear.weightTorusCoordinateMap wt

The subsystem defining ideal is the common-kernel Hopf ideal of the selected root-subgroup coordinate maps and the weight-torus coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.le_kostantTorusSubsystemDefiningIdeal_iff {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) : J ≤ kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS ↔ (∀ (i : I) (hi : i ∈ S), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b))).toRingHom) ∧ J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap wt))).toRingHom

A Hopf ideal lies in the subsystem defining ideal exactly when the selected root-subgroup maps and the weight-torus map kill it. This is the coordinate universal property of the closed carrier.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal_anti {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {S T : Set I} (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hnilT : ∀ (i : ↑T), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hST : S ⊆ T) : kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt T hnilT ≤ kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS

Enlarging the selected set can only shrink its common-kernel defining ideal. Equivalently, the associated closed subgroup scheme grows with the selected root set.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralDefiningIdeal_le_kostantTorusSubsystemDefiningIdeal {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) : kostantToralDefiningIdeal e h ρ M hM hnil b wt ≤ kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S ⋯

The full toral defining ideal lies in every subsystem defining ideal.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal_univ {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))} : kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt Set.univ ⋯ = kostantToralDefiningIdeal e h ρ M hM hnil b wt

Selecting every root subgroup recovers the defining ideal of the full toral closure.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal_toIdeal_le_root_ker {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) {i : I} (hi : i ∈ S) : (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b))).toRingHom

Every selected represented root-subgroup coordinate map kills the subsystem defining ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemDefiningIdeal_toIdeal_le_torus_ker {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap wt))).toRingHom

The represented weight-torus coordinate map kills every subsystem defining ideal.

@[reducible, inline]

noncomputable abbrev TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupScheme {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The affine group scheme generated by the selected root subgroups and the weight torus.

Equations

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupSchemeι {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : kostantTorusSubsystemGroupScheme e h ρ M hM b wt S hnilS ⟶ GeneralLinear.groupScheme ℤ n

The inclusion of a torus-subsystem carrier into GLₙ.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupSchemeι_def {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : kostantTorusSubsystemGroupSchemeι e h ρ M hM b wt S hnilS = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS)) (CategoryTheory.eqToHom ⋯)

The subsystem inclusion is the quotient-spectrum inclusion transported across the named presentation of GLₙ.

instance TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantTorusSubsystemGroupSchemeι {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantTorusSubsystemGroupSchemeι e h ρ M hM b wt S hnilS).hom.hom)

The torus-subsystem inclusion into GLₙ is a closed immersion.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMapOfSubset {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {S T : Set I} (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hnilT : ∀ (i : ↑T), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hST : S ⊆ T) : kostantTorusSubsystemGroupScheme e h ρ M hM b wt S hnilS ⟶ kostantTorusSubsystemGroupScheme e h ρ M hM b wt T hnilT

An inclusion S ⊆ T induces the closed immersion from the carrier generated by S into the carrier generated by T.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilS hnilT hST = TauCeti.CommHopfAlgCat.quotientSpecMapOfLe (TauCeti.GeneralLinear.coordinateHopfAlgebra ℤ n) ⋯

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMapOfSubset_refl {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hSS : S ⊆ S) : kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilS hnilS hSS = CategoryTheory.CategoryStruct.id (kostantTorusSubsystemGroupScheme e h ρ M hM b wt S hnilS)

The subsystem map induced by a reflexive set inclusion is the identity.

instance TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantTorusSubsystemMapOfSubset {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {S T : Set I} (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hnilT : ∀ (i : ↑T), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hST : S ⊆ T) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilS hnilT hST).hom.hom)

The map induced by inclusion of selected root sets is a closed immersion.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMapOfSubset_comp_ι {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {S T : Set I} (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hnilT : ∀ (i : ↑T), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hST : S ⊆ T) : CategoryTheory.CategoryStruct.comp (kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilS hnilT hST) (kostantTorusSubsystemGroupSchemeι e h ρ M hM b wt T hnilT) = kostantTorusSubsystemGroupSchemeι e h ρ M hM b wt S hnilS

The inclusion induced by S ⊆ T, followed by the inclusion into GLₙ, is the direct inclusion of the S-carrier.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMapOfSubset_comp {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {S T U : Set I} (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hnilT : ∀ (i : ↑T), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hnilU : ∀ (i : ↑U), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hST : S ⊆ T) (hTU : T ⊆ U) : CategoryTheory.CategoryStruct.comp (kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilS hnilT hST) (kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilT hnilU hTU) = kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilS hnilU ⋯

Closed subsystem inclusions compose along inclusions of selected root sets.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemToToral {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) : kostantTorusSubsystemGroupScheme e h ρ M hM b wt S ⋯ ⟶ kostantToralGroupScheme e h ρ M hM hnil b wt

The torus-subsystem carrier as a closed subgroup scheme of the full toral closure.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemToToral e h ρ M hM b wt hnil S = TauCeti.CommHopfAlgCat.quotientSpecMapOfLe (TauCeti.GeneralLinear.coordinateHopfAlgebra ℤ n) ⋯

instance TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantTorusSubsystemToToral {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantTorusSubsystemToToral e h ρ M hM b wt hnil S).hom.hom)

The subsystem carrier includes into the full toral closure as a closed immersion.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemToToral_comp_ι {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) : CategoryTheory.CategoryStruct.comp (kostantTorusSubsystemToToral e h ρ M hM b wt hnil S) (kostantToralGroupSchemeι e h ρ M hM hnil b wt) = kostantTorusSubsystemGroupSchemeι e h ρ M hM b wt S ⋯

The subsystem inclusion followed by the full toral inclusion is its direct inclusion into GLₙ.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemMapOfSubset_comp_kostantTorusSubsystemToToral {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {S T : Set I} (hST : S ⊆ T) : CategoryTheory.CategoryStruct.comp (kostantTorusSubsystemMapOfSubset e h ρ M hM b wt ⋯ ⋯ hST) (kostantTorusSubsystemToToral e h ρ M hM b wt hnil T) = kostantTorusSubsystemToToral e h ρ M hM b wt hnil S

The map induced by S ⊆ T, followed by the inclusion of the T-carrier into the full toral closure, is the inclusion of the S-carrier.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemClosedSubgroup {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) : ClosedSubgroupScheme (kostantToralGroupScheme e h ρ M hM hnil b wt)

A torus-subsystem carrier, regarded as a closed subgroup scheme of the full toral closure.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantTorusSubsystemClosedSubgroup {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) : ↑(kostantTorusSubsystemClosedSubgroup e h ρ M hM b wt hnil S) = CategoryTheory.Subobject.mk (kostantTorusSubsystemToToral e h ρ M hM b wt hnil S)

The underlying subobject of a torus subsystem is represented by its canonical inclusion.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemClosedSubgroup_mono {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {S T : Set I} (hST : S ⊆ T) : kostantTorusSubsystemClosedSubgroup e h ρ M hM b wt hnil S ≤ kostantTorusSubsystemClosedSubgroup e h ρ M hM b wt hnil T

Inclusion of selected root sets gives inclusion of the corresponding closed subgroup schemes of the full toral closure.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupTorusSubsystemCoordinateMap {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) {i : I} (hi : i ∈ S) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS) ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The coordinate map through which a selected root subgroup factors into its subsystem carrier.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantRootSubgroupTorusSubsystemCoordinateMap {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) {i : I} (hi : i ∈ S) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS)) (kostantRootSubgroupTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS hi) = kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b

The selected root-subgroup factorization recovers its represented coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupTorusSubsystemCoordinateMap_surjective_of_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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) {i : I} (hi : i ∈ S) (hroot : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b))) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS hi))

A surjective selected root-subgroup coordinate map remains surjective after factoring through the subsystem carrier.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusTorusSubsystemCoordinateMap {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS) ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj

The coordinate map through which the weight torus factors into a subsystem carrier.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantWeightTorusTorusSubsystemCoordinateMap {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS)) (kostantWeightTorusTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS) = GeneralLinear.weightTorusCoordinateMap wt

The weight-torus factorization recovers its represented coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemCoordinate_hom_ext {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {Y : CommHopfAlgCat ℤ} (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (u v : Y ⟶ CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS)) (hroot : ∀ (i : I) (hi : i ∈ S), CategoryTheory.CategoryStruct.comp u (kostantRootSubgroupTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS hi) = CategoryTheory.CategoryStruct.comp v (kostantRootSubgroupTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS hi)) (htorus : CategoryTheory.CategoryStruct.comp u (kostantWeightTorusTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS) = CategoryTheory.CategoryStruct.comp v (kostantWeightTorusTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS)) : u = v

Coordinate rigidity of a torus-subsystem carrier. Two morphisms into its coordinate algebra are equal when they agree after composition with every selected root coordinate and with the weight-torus coordinate.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToTorusSubsystem {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) {i : I} (hi : i ∈ S) : AdditiveGroup.groupScheme ℤ ⟶ kostantTorusSubsystemGroupScheme e h ρ M hM b wt S hnilS

A selected represented Kostant root subgroup, factored through the subsystem carrier.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToTorusSubsystem_def {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) {i : I} (hi : i ∈ S) : kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S hnilS hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.hopfSpec ↧ℤ).map (kostantRootSubgroupTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS hi).op)

A selected root-subgroup morphism into its subsystem carrier is the spectrum map of its factored coordinate morphism, after the canonical presentation of the additive group.

theorem TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantRootSubgroupToTorusSubsystem_of_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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) {i : I} (hi : i ∈ S) (hroot : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS hi))) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S hnilS hi).hom.hom)

A selected root-subgroup morphism into its subsystem carrier is a closed immersion whenever its factored coordinate map is surjective.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToTorusSubsystem_comp_ι {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) {i : I} (hi : i ∈ S) : CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S hnilS hi) (kostantTorusSubsystemGroupSchemeι e h ρ M hM b wt S hnilS) = kostantRootSubgroup e h ρ M hM i ⋯ b

Factoring a selected root subgroup through its subsystem carrier and then including into GLₙ recovers the represented root-subgroup morphism.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToTorusSubsystem_comp_mapOfSubset {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {S T : Set I} (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hnilT : ∀ (i : ↑T), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hST : S ⊆ T) {i : I} (hi : i ∈ S) : CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S hnilS hi) (kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilS hnilT hST) = kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt T hnilT ⋯

Factoring a selected root subgroup through nested subsystem carriers is natural in the selected root set.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToTorusSubsystem_comp_kostantTorusSubsystemToToral {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) {i : I} (hi : i ∈ S) : CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S ⋯ hi) (kostantTorusSubsystemToToral e h ρ M hM b wt hnil S) = kostantRootSubgroupToToral e h ρ M hM hnil b wt i

Factoring a selected root subgroup through its subsystem and then into the full toral closure agrees with the direct toral factorization.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToTorusSubsystem {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : SplitTorus.groupScheme ℤ κ ⟶ kostantTorusSubsystemGroupScheme e h ρ M hM b wt S hnilS

The represented weight torus, factored through a torus-subsystem carrier.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToTorusSubsystem_def {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((AlgebraicGeometry.hopfSpec ↧ℤ).map (kostantWeightTorusTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS).op)

The weight-torus morphism into a subsystem carrier is the spectrum map of its factored coordinate morphism, after the canonical presentation of the split torus.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusTorusSubsystemCoordinateMap_surjective_of_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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (htorus : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusCoordinateMap wt))) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantWeightTorusTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS))

A surjective represented weight-torus coordinate map remains surjective after factoring through a subsystem carrier.

theorem TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantWeightTorusToTorusSubsystem_of_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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (htorus : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (kostantWeightTorusTorusSubsystemCoordinateMap e h ρ M hM b wt S hnilS))) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS).hom.hom)

The represented weight torus is a closed subgroup of its subsystem carrier whenever its factored coordinate map is surjective.

theorem TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantWeightTorusToTorusSubsystem {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS).hom.hom)

Spanning weights represent the weight torus as a closed subgroup of every subsystem carrier.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToTorusSubsystem_comp_ι {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : CategoryTheory.CategoryStruct.comp (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS) (kostantTorusSubsystemGroupSchemeι e h ρ M hM b wt S hnilS) = GeneralLinear.weightTorus wt

Factoring the weight torus through a subsystem carrier and then including into GLₙ recovers the represented weight-torus morphism.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToTorusSubsystem_comp_mapOfSubset {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {S T : Set I} (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hnilT : ∀ (i : ↑T), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (hST : S ⊆ T) : CategoryTheory.CategoryStruct.comp (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS) (kostantTorusSubsystemMapOfSubset e h ρ M hM b wt hnilS hnilT hST) = kostantWeightTorusToTorusSubsystem e h ρ M hM b wt T hnilT

Factoring the weight torus through nested subsystem carriers is natural in the selected root set.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToTorusSubsystem_comp_kostantTorusSubsystemToToral {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) : CategoryTheory.CategoryStruct.comp (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S ⋯) (kostantTorusSubsystemToToral e h ρ M hM b wt hnil S) = kostantWeightTorusToToral e h ρ M hM hnil b wt

Factoring the weight torus through a subsystem and then into the full toral closure agrees with the direct toral factorization.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemClosedSubgroup_le_iff {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (S : Set I) (P : ClosedSubgroupScheme (kostantToralGroupScheme e h ρ M hM hnil b wt)) : kostantTorusSubsystemClosedSubgroup e h ρ M hM b wt hnil S ≤ P ↔ (∀ i ∈ S, ∃! f : AdditiveGroup.groupScheme ℤ ⟶ CategoryTheory.Subobject.underlying.obj ↑P, CategoryTheory.CategoryStruct.comp f (↑P).arrow = kostantRootSubgroupToToral e h ρ M hM hnil b wt i) ∧ ∃! f : SplitTorus.groupScheme ℤ κ ⟶ CategoryTheory.Subobject.underlying.obj ↑P, CategoryTheory.CategoryStruct.comp f (↑P).arrow = kostantWeightTorusToToral e h ρ M hM hnil b wt

Universal property of the torus-subsystem carrier. It is the smallest closed subgroup scheme of the full toral closure through which every selected root-subgroup morphism and the weight-torus morphism factor. Each factorization is unique because the arrow representing a closed subgroup is a monomorphism.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupScheme_hom_ext {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) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) {Y : CommHopfAlgCat ℤ} (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) (φ ψ : kostantTorusSubsystemGroupScheme e h ρ M hM b wt S hnilS ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (i : I) (hi : i ∈ S), CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S hnilS hi) φ = CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S hnilS hi) ψ) (htorus : CategoryTheory.CategoryStruct.comp (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS) φ = CategoryTheory.CategoryStruct.comp (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS) ψ) : φ = ψ

Rigidity of a torus-subsystem group scheme. Two homomorphisms out of the subsystem carrier are equal when they agree on every selected root subgroup and on the weight torus.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemGroupScheme_hom_ext_iff {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} {n : ℕ} {b : Module.Basis (Fin n) ℤ ↥M} {wt : Fin n → κ → ℤ} {Y : CommHopfAlgCat ℤ} {S : Set I} {hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))} {φ ψ : kostantTorusSubsystemGroupScheme e h ρ M hM b wt S hnilS ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : φ = ψ ↔ (∀ (i : I) (hi : i ∈ S), CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S hnilS hi) φ = CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToTorusSubsystem e h ρ M hM b wt S hnilS hi) ψ) ∧ CategoryTheory.CategoryStruct.comp (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS) φ = CategoryTheory.CategoryStruct.comp (kostantWeightTorusToTorusSubsystem e h ρ M hM b wt S hnilS) ψ