The closed group scheme generated by a Kostant torus and root subgroups

Fix a finite free Kostant-stable lattice with a basis, and prescribe an integer weight for each basis vector. Distinguished nilpotent vectors give represented root-subgroup morphisms xᵢ : 𝔾ₐ → GLₙ, while the chosen weights give a represented split-torus morphism T → GLₙ. This file constructs the smallest closed subgroup scheme of GLₙ containing both families.

On coordinate Hopf algebras, the defining ideal is the largest Hopf ideal killed by every root subgroup coordinate map and by the weight-torus coordinate map. Quotienting by that ideal gives an explicit affine group scheme, and both the root subgroups and the torus factor through it. The previously constructed root-generated group scheme is a closed subgroup scheme of this toral closure.

For arbitrary vectors and weights, no maximality of the torus and no reductivity or Borel structure is asserted. When the inputs come from a Chevalley system and an admissible weight lattice, this is the carrier assembled from the torus and root subgroups in the Chevalley--Demazure construction. The remaining pinning work must identify the appropriate Borel and prove the root-datum properties.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantToralDefiningIdeal: the common-kernel Hopf ideal of the root-subgroup and weight-torus coordinate maps.
• TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme: the resulting closed subgroup scheme of GLₙ.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToToral: the factored root-subgroup morphisms.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToToral: the factored weight-torus morphism.
• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedToToral: the closed immersion from the root-generated group scheme.

References

The construction is the scheme-theoretic closure of the torus and root subgroups used in the Chevalley--Demazure construction; see J. E. Humphreys, Linear Algebraic Groups, §26, and R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1. It advances Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md and supplies the assembled ambient carrier required by milestone L0 of the CFSGStatement roadmap.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralDefiningIdeal {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 → κ → ℤ) : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)

The defining Hopf ideal of the closed subgroup scheme generated jointly by the represented Kostant root subgroups and the represented weight torus. It is the largest Hopf ideal killed by all of those coordinate maps.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.le_kostantToralDefiningIdeal_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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → κ → ℤ) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) : J ≤ kostantToralDefiningIdeal e h ρ M hM hnil b wt ↔ (∀ (i : I), 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 toral defining ideal exactly when every root-subgroup coordinate map and the weight-torus coordinate map kill it.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralDefiningIdeal_comapOfSurjective_le_of_comp_eq {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 → κ → ℤ) (φ : GeneralLinear.coordinateHopfAlgebra ℤ n ⟶ GeneralLinear.coordinateHopfAlgebra ℤ n) (hφ : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom φ)) (s : I → I) (t : (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj) (ht : Function.Injective ⇑(CommHopfAlgCat.Hom.hom t)) (hroot : ∀ (i : I), CategoryTheory.CategoryStruct.comp φ (kostantRootSubgroupCoordinateMap e h ρ M hM (s i) ⋯ b) = kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b) (htorus : CategoryTheory.CategoryStruct.comp φ (GeneralLinear.weightTorusCoordinateMap wt) = CategoryTheory.CategoryStruct.comp (GeneralLinear.weightTorusCoordinateMap wt) t) : (kostantToralDefiningIdeal e h ρ M hM hnil b wt).comapOfSurjective (CommHopfAlgCat.Hom.hom φ) hφ ≤ kostantToralDefiningIdeal e h ρ M hM hnil b wt

A surjective endomorphism of the ambient coordinate Hopf algebra which reindexes the root-subgroup coordinate maps and carries the weight-torus coordinate map to itself up to an injective postcomposition pulls the toral defining ideal into itself.

The conclusion is one containment, not invariance: an automorphism fixing the ideal needs this lemma once for itself and once for its inverse.

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

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

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

The represented weight-torus coordinate map kills the toral defining ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralDefiningIdeal_le_kostantGeneratedDefiningIdeal {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 → κ → ℤ) : kostantToralDefiningIdeal e h ρ M hM hnil b wt ≤ kostantGeneratedDefiningIdeal e h ρ M hM hnil b

Adding the weight torus to the generators can only shrink the defining ideal. Equivalently, the root-generated group scheme is a closed subgroup scheme of the toral closure.

@[reducible, inline]

noncomputable abbrev TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme {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 → κ → ℤ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The affine group scheme generated jointly by the represented Kostant root subgroups and weight torus, presented as a Hopf-ideal quotient of the coordinate algebra of GLₙ.

Equations

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupSchemeι {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 → κ → ℤ) : kostantToralGroupScheme e h ρ M hM hnil b wt ⟶ GeneralLinear.groupScheme ℤ n

The toral closure is a closed subgroup scheme of GLₙ.

Equations

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

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

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

instance TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantToralGroupSchemeι {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 → κ → ℤ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantToralGroupSchemeι e h ρ M hM hnil b wt).hom.hom)

The inclusion of the toral closure into GLₙ is a closed immersion.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap {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 → κ → ℤ) (i : I) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt) ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The coordinate map through which the ith root subgroup factors into the toral closure.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantRootSubgroupToralCoordinateMap {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 → κ → ℤ) (i : I) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)) (kostantRootSubgroupToralCoordinateMap e h ρ M hM hnil b wt i) = kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b

Composing the quotient morphism with a factored root coordinate map recovers the represented root-subgroup coordinate map.

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

A surjective root-subgroup coordinate map remains surjective after factoring through the toral closure.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToralCoordinateMap {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 → κ → ℤ) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt) ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj

The coordinate map through which the represented weight torus factors into the toral closure.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantWeightTorusToralCoordinateMap {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 → κ → ℤ) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)) (kostantWeightTorusToralCoordinateMap e h ρ M hM hnil b wt) = GeneralLinear.weightTorusCoordinateMap wt

Composing the quotient morphism with the factored torus coordinate map recovers the weight torus coordinate map.

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

The ith represented Kostant root subgroup, factored through the toral closure.

Equations

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

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

The root-subgroup morphism into the toral closure is the spectrum map of its factored coordinate morphism, after the canonical identification of the additive group scheme.

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

A root-subgroup morphism into the toral closure is a closed immersion whenever its factored coordinate map is surjective.

@[simp]

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

Factoring a root subgroup through the toral closure and then including into GLₙ recovers the original represented root-subgroup morphism.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.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 → κ → ℤ) : SplitTorus.groupScheme ℤ κ ⟶ kostantToralGroupScheme e h ρ M hM hnil b wt

The represented Kostant weight torus, factored through the toral closure.

Equations

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

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

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

@[simp]

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

Factoring the weight torus through the toral closure and then including into GLₙ recovers the original represented weight-torus morphism.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedToToral {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 → κ → ℤ) : kostantGeneratedGroupScheme e h ρ M hM hnil b ⟶ kostantToralGroupScheme e h ρ M hM hnil b wt

The root-generated Kostant group scheme as a closed subgroup scheme of the toral closure.

Equations

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

instance TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantGeneratedToToral {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 → κ → ℤ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantGeneratedToToral e h ρ M hM hnil b wt).hom.hom)

The root-generated carrier includes into the toral closure as a closed immersion.

@[simp]

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

The inclusion of the root-generated carrier into the toral closure, followed by the toral inclusion into GLₙ, is the original root-generated inclusion.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToGenerated_comp_kostantGeneratedToToral {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 → κ → ℤ) (i : I) : CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToGenerated e h ρ M hM hnil b i) (kostantGeneratedToToral e h ρ M hM hnil b wt) = kostantRootSubgroupToToral e h ρ M hM hnil b wt i

Factoring a root subgroup first through the root-generated carrier and then through its closed immersion into the toral closure agrees with the direct toral factorization.