Base change of the toral Kostant closure

The toral Kostant closure over ℤ is the closed subgroup scheme of GLₙ generated jointly by the represented root subgroups and a represented split torus. Its coordinate ring is the general-linear coordinate Hopf algebra modulo kostantToralDefiningIdeal.

This file transports that presentation along ℤ → A. The base-changed defining ideal cuts out the specialized carrier, its quotient is canonically the base change of the original coordinate ring, and the factored root-subgroup and torus maps base-change without being chosen again.

The construction deliberately stays in the base-changed coordinate algebras. Identifying the base change of O(GLₙ/ℤ), O(𝔾ₐ/ℤ), and O(T/ℤ) with the corresponding coordinate Hopf algebras constructed directly over A is the next, independent comparison step.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIdeal: the base change of the ideal defining the toral closure.
• TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIso: the quotient by that ideal is the base change of the toral closure's coordinate ring.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralBaseChangeCoordinateMap: the base-changed factored root-subgroup map.
• TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToralBaseChangeCoordinateMap: the base-changed factored torus map.

References

This is the base-change compatibility in the pinned Chevalley--Demazure construction; see R. W. Carter, Simple Groups of Lie Type, §4.4, and B. Conrad, Reductive Group Schemes, §1. It advances Layer 9 of the ReductiveGroups roadmap, whose base-changed pinned carrier is consumed by milestone L0 of the CFSGStatement roadmap.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIdeal {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 → κ → ℤ) (A : Type u_1) [CommRing A] : HopfIdeal A ↑(CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))

The base change along ℤ → A of the Hopf ideal defining the toral Kostant closure.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIdeal_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 → κ → ℤ) (A : Type u_1) [CommRing A] : kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A = CommHopfAlgCat.baseChangeHopfIdeal (kostantToralDefiningIdeal e h ρ M hM hnil b wt)

The specialized defining ideal is the generic base change of the ideal of the toral closure over ℤ.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIso {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 → κ → ℤ) (A : Type u_1) [CommRing A] : CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt))

Quotienting by the specialized toral ideal agrees with base-changing the coordinate ring of the toral closure.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantToralBaseChangeIso_hom {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 → κ → ℤ) (A : Type u_1) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A)) (kostantToralBaseChangeIso e h ρ M hM hnil b wt A).hom = CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt))

The base-change identification is compatible with the quotient morphism presenting the toral closure over ℤ.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralBaseChangeCoordinateMap {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 → κ → ℤ) (A : Type u_1) [CommRing A] (i : I) : CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A) ⟶ CommHopfAlgCat.baseChange (AdditiveGroup.coordinateHopfAlgebra ℤ)

The ith factored root-subgroup coordinate map after base change: the base change of the map into the toral closure, read through its specialized quotient presentation.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIso_inv_comp_rootSubgroupToralBaseChangeCoordinateMap {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 → κ → ℤ) (A : Type u_1) [CommRing A] (i : I) : CategoryTheory.CategoryStruct.comp (kostantToralBaseChangeIso e h ρ M hM hnil b wt A).inv (kostantRootSubgroupToralBaseChangeCoordinateMap e h ρ M hM hnil b wt A i) = CommHopfAlgCat.baseChangeMap (kostantRootSubgroupToralCoordinateMap e h ρ M hM hnil b wt i)

Reading a root-subgroup map back through the toral base-change comparison recovers the scalar extension of its integral factorization.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantRootSubgroupToralBaseChangeCoordinateMap {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 → κ → ℤ) (A : Type u_1) [CommRing A] (i : I) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A)) (kostantRootSubgroupToralBaseChangeCoordinateMap e h ρ M hM hnil b wt A i) = CommHopfAlgCat.baseChangeMap (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)

The specialized quotient map followed by the factored root-subgroup map is the base change of the original represented root-subgroup coordinate map.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToralBaseChangeCoordinateMap {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 → κ → ℤ) (A : Type u_1) [CommRing A] : CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A) ⟶ CommHopfAlgCat.baseChange (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup κ)).obj

The factored weight-torus coordinate map after base change: the base change of the map into the toral closure, read through its specialized quotient presentation.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIso_inv_comp_weightTorusToralBaseChangeCoordinateMap {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 → κ → ℤ) (A : Type u_1) [CommRing A] : CategoryTheory.CategoryStruct.comp (kostantToralBaseChangeIso e h ρ M hM hnil b wt A).inv (kostantWeightTorusToralBaseChangeCoordinateMap e h ρ M hM hnil b wt A) = CommHopfAlgCat.baseChangeMap (kostantWeightTorusToralCoordinateMap e h ρ M hM hnil b wt)

Reading the weight-torus map back through the toral base-change comparison recovers the scalar extension of its integral factorization.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantWeightTorusToralBaseChangeCoordinateMap {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 → κ → ℤ) (A : Type u_1) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A)) (kostantWeightTorusToralBaseChangeCoordinateMap e h ρ M hM hnil b wt A) = CommHopfAlgCat.baseChangeMap (GeneralLinear.weightTorusCoordinateMap wt)

The specialized quotient map followed by the factored weight-torus map is the base change of the original represented weight-torus coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIdeal_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 → κ → ℤ) (A : Type u_1) [CommRing A] (i : I) : (kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.baseChangeMap (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)))).toRingHom

Every base-changed represented root-subgroup map kills the specialized toral defining ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIdeal_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 → κ → ℤ) (A : Type u_1) [CommRing A] : (kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.baseChangeMap (GeneralLinear.weightTorusCoordinateMap wt)))).toRingHom

The base-changed represented weight-torus map kills the specialized toral defining ideal.