Base change of the group scheme generated by Kostant root subgroups

The Chevalley carrier G generated by the represented Kostant root subgroups is a closed subgroup scheme of GLₙ over ℤ, presented as the quotient of the general-linear coordinate Hopf algebra by the Hopf ideal J common to the kernels of all root-subgroup coordinate maps. This file transports that presentation along ℤ → A for an arbitrary commutative ring A.

The base change G_A is cut out inside the base change of the ambient general-linear coordinate algebra by the base-changed Hopf ideal J_A, and the base change of each root subgroup still factors through it, with the same factorization the construction over ℤ provides. That is the compatibility of the root-subgroup coordinate maps with base change: their factorizations do not have to be rechosen over A.

Generation, on the other hand, only transports in one direction: the carrier generated over A by the base-changed root subgroups is a closed subgroup scheme of G_A (kostantGeneratedBaseChangeIdeal_le_commonKernelHopfIdeal), and equality is not claimed, since a Hopf ideal of A ⊗[ℤ] O(GLₙ) killed by every base-changed root-subgroup map need not descend.

The second half of the file removes the tensor factor from the ambient group. Transporting the presentation along A ⊗[ℤ] O(GLₙ) ≅ O(GLₙ over A) exhibits G_A as a closed subgroup scheme of GLₙ over A itself, cut out by the Hopf ideal kostantGeneratedGeneralLinearBaseChangeIdeal, and each base-changed root subgroup becomes a morphism 𝔾ₐ → G_A of group schemes over A after the same identification is made on the additive coordinate algebra. This is the form a consumer working in a fixed characteristic asks for: it base-changes the Chevalley carrier to 𝔽_p or to an algebraic closure and wants a subgroup scheme of the general linear group over that field, not of a scalar extension of the general linear group over ℤ.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedBaseChangeIdeal: the base change J_A of the defining Hopf ideal.
• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedBaseChangeIso: the base change of the carrier is the quotient by J_A.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangeGeneratedCoordinateMap: the base-changed root subgroup, factored through the base-changed carrier.
• mkQuotient_comp_kostantRootSubgroupBaseChangeGeneratedCoordinateMap: the factorization recovers the base change of the root-subgroup coordinate map.
• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedBaseChangeIdeal_le_commonKernelHopfIdeal: the carrier generated over A lies inside the base-changed carrier.
• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal: the Hopf ideal of the general-linear coordinate algebra over A which presents the base-changed carrier.
• TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIso: that presentation is the base change of the carrier over ℤ.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupGeneralLinearBaseChangeCoordinateMap: the base-changed root subgroup over A.
• kostantGeneratedGeneralLinearBaseChangeIdeal_le_commonKernelHopfIdeal: over A too, the carrier generated by the root subgroups lies inside the base-changed carrier.

References

This advances the Layer 9 milestone "base change along ℤ → k for any commutative ring k, and the compatibility of the pinning with it" of TauCetiRoadmap/ReductiveGroups/README.md, which milestone L0 of the CFSGStatement roadmap consumes when it base-changes a pinned Chevalley--Demazure group to a prime field and its algebraic closure. See R. W. Carter, Simple Groups of Lie Type, §4.4, and B. Conrad, Reductive Group Schemes, §1.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedBaseChangeIdeal {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : HopfIdeal A ↑(CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))

The base change along ℤ → A of the Hopf ideal defining the Chevalley carrier generated by the represented Kostant root subgroups.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedBaseChangeIdeal_def {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : kostantGeneratedBaseChangeIdeal e h ρ M hM hnil b A = CommHopfAlgCat.baseChangeHopfIdeal (kostantGeneratedDefiningIdeal e h ρ M hM hnil b)

The specialized base-changed defining ideal is the generic base change of the ideal defining the Chevalley carrier over ℤ.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedBaseChangeIso {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantGeneratedBaseChangeIdeal e h ρ M hM hnil b A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantGeneratedDefiningIdeal e h ρ M hM hnil b))

The base change of the Chevalley carrier is the quotient of the base-changed general-linear coordinate algebra by the base-changed defining ideal: base change of the group scheme and of its presentation as a closed subgroup scheme agree.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantGeneratedBaseChangeIso_hom {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantGeneratedBaseChangeIdeal e h ρ M hM hnil b A)) (kostantGeneratedBaseChangeIso e h ρ M hM hnil b A).hom = CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantGeneratedDefiningIdeal e h ρ M hM hnil b))

The specialized identification of the base-changed carrier is compatible with the quotient morphism presenting the carrier over ℤ.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangeGeneratedCoordinateMap {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (i : I) : CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantGeneratedBaseChangeIdeal e h ρ M hM hnil b A) ⟶ CommHopfAlgCat.baseChange (AdditiveGroup.coordinateHopfAlgebra ℤ)

The ith base-changed root-subgroup coordinate map, factored through the base change of the Chevalley carrier: the base change of the factorization over ℤ, read through the presentation of the base change.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantRootSubgroupBaseChangeGeneratedCoordinateMap {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (i : I) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n)) (kostantGeneratedBaseChangeIdeal e h ρ M hM hnil b A)) (kostantRootSubgroupBaseChangeGeneratedCoordinateMap e h ρ M hM hnil b A i) = CommHopfAlgCat.baseChangeMap (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)

Quotienting by the base-changed defining ideal and then applying the base-changed factored root subgroup recovers the base change of the ith root-subgroup coordinate map. This is the compatibility of the root-subgroup data with base change.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedBaseChangeIdeal_toIdeal_le_ker {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (i : I) : (kostantGeneratedBaseChangeIdeal e h ρ M hM hnil b A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.baseChangeMap (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)))).toRingHom

Every base-changed root-subgroup coordinate map kills the base-changed defining ideal, so the base-changed root subgroups all land in the base change of the Chevalley carrier.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedBaseChangeIdeal_le_commonKernelHopfIdeal {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : kostantGeneratedBaseChangeIdeal e h ρ M hM hnil b A ≤ CommHopfAlgCat.commonKernelHopfIdeal fun (i : I) => CommHopfAlgCat.baseChangeMap (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)

The Chevalley carrier generated over A by the base-changed root subgroups is a closed subgroup scheme of the base change of the carrier generated over ℤ.

The reverse containment is not claimed: it asks a Hopf ideal of A ⊗[ℤ] O(GLₙ) killed by every base-changed root-subgroup coordinate map to descend to ℤ.

The presentation inside the general linear group over the new base

Base change of the ambient general linear group is GLₙ over the new base, so the presentation above can be read there. The identification used is TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso on the ambient group and TauCeti.AdditiveGroup.coordinateHopfAlgebraBaseChangeIso on the parameter group.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A n)

The Hopf ideal of the general-linear coordinate algebra over A which presents the base change of the Chevalley carrier: the inverse image of the base-changed defining ideal under the identification of O(GLₙ) over A with A ⊗[ℤ] O(GLₙ).

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantGeneratedGeneralLinearBaseChangeIdeal_iff {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] {x : ↑(GeneralLinear.coordinateHopfAlgebra A n)} : x ∈ kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A n).inv) x ∈ kostantGeneratedBaseChangeIdeal e h ρ M hM hnil b A

Membership in the general-linear defining ideal over A is membership of the transported element in the base-changed defining ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.map_tmul_mem_kostantGeneratedGeneralLinearBaseChangeIdeal_of_mem {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (s : A) {y : ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)} (hy : y ∈ kostantGeneratedDefiningIdeal e h ρ M hM hnil b) : (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A n).hom) (s ⊗ₜ[ℤ] y) ∈ kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A

The transported pure tensor of every scalar and defining equation over ℤ belongs to the general-linear base-change ideal over A.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIso {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A n) (kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantGeneratedDefiningIdeal e h ρ M hM hnil b))

The Chevalley carrier presented inside GLₙ over A is the base change of the Chevalley carrier over ℤ.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantGeneratedGeneralLinearBaseChangeIso_hom {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A n) (kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A)) (kostantGeneratedGeneralLinearBaseChangeIso e h ρ M hM hnil b A).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A n).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantGeneratedDefiningIdeal e h ρ M hM hnil b)))

The identification of the carrier presented over A with the base change of the carrier over ℤ is compatible with the two quotient morphisms.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupGeneralLinearBaseChangeCoordinateMap {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 : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_3) [CommRing A] : GeneralLinear.coordinateHopfAlgebra A n ⟶ AdditiveGroup.coordinateHopfAlgebra A

The ith base-changed root subgroup, read as a morphism of coordinate Hopf algebras over A: a morphism 𝔾ₐ → GLₙ of group schemes over A.

Equations

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupGeneralLinearBaseChangeGeneratedCoordinateMap {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (i : I) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A n) (kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

The ith base-changed root subgroup over A, factored through the Chevalley carrier presented inside GLₙ over A.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantRootSubgroupGeneralLinearBaseChangeGeneratedCoordinateMap {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (i : I) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A n) (kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A)) (kostantRootSubgroupGeneralLinearBaseChangeGeneratedCoordinateMap e h ρ M hM hnil b A i) = kostantRootSubgroupGeneralLinearBaseChangeCoordinateMap e h ρ M hM i ⋯ b A

Quotienting by the general-linear defining ideal over A and then applying the factored root subgroup recovers the base-changed root subgroup itself. This is the compatibility of the root-subgroup data with base change, stated over A throughout.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal_toIdeal_le_ker {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] (i : I) : (kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupGeneralLinearBaseChangeCoordinateMap e h ρ M hM i ⋯ b A))).toRingHom

Every root subgroup over A kills the general-linear defining ideal over A, so all of them land in the Chevalley carrier presented there.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedGeneralLinearBaseChangeIdeal_le_commonKernelHopfIdeal {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) (hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (A : Type u_2) [CommRing A] : kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A ≤ CommHopfAlgCat.commonKernelHopfIdeal fun (i : I) => kostantRootSubgroupGeneralLinearBaseChangeCoordinateMap e h ρ M hM i ⋯ b A

The Chevalley carrier generated over A by the root subgroups over A is a closed subgroup scheme of the base change of the carrier over ℤ, now inside GLₙ over A.

As over the base-changed ambient group, the reverse containment is not claimed.