The base-changed toral Kostant closure inside the general linear group

The toral Kostant closure over ℤ is the closed subgroup scheme of GLₙ generated jointly by represented root subgroups and a represented split torus. Base change first presents it inside the scalar extension A ⊗[ℤ] O(GLₙ/ℤ). This file transports that presentation across the canonical Hopf-algebra isomorphism

A ⊗[ℤ] O(GLₙ/ℤ) ≅ O(GLₙ/A),

so the carrier is cut out directly inside GLₙ over A. The root-subgroup parameter algebra and the split-torus coordinate algebra are transported at the same time. Consequently the factored maps have target O(𝔾ₐ/A) and O(T/A), rather than scalar extensions of the corresponding coordinate algebras over ℤ. The Presentation in the names records exactly this: these objects live in the coordinate algebras built directly over A, whereas the kostantToralBaseChange* family of ToralClosure/BaseChange.lean lives in the scalar extensions of the integral ones.

Everything here is a transport of the integral data, not a fresh construction over A. The underlying bialgebra morphism of the transported split-torus map is identified with GeneralLinear.weightTorusCoordinateBialgHom, constructed directly over A; this formulation also covers value rings in a larger universe than the integral torus index. On the root-subgroup side no over-A construction exists yet.

The transported ideal need not be the largest Hopf ideal killed by the root subgroups and torus after base change: new equations may appear over a non-flat base. The proved comparison therefore has the honest direction only. The closed subgroup generated over A by the transported root and torus maps lies in the base change of the integral toral carrier; equality is not asserted.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal: the transported defining ideal in O(GLₙ/A).
• kostantToralBaseChangePresentationIso: its quotient is the base change of the integral toral coordinate ring.
• kostantRootSubgroupBaseChangePresentationCoordinateMap and kostantRootSubgroupToralBaseChangePresentationCoordinateMap: the transported base change of a root subgroup and its factorization through the transported toral carrier.
• kostantWeightTorusToralBaseChangePresentationCoordinateMap: the factorization of the transported weight-torus coordinate map through the transported carrier.
• kostantToralBaseChangePresentationIdeal_le_commonKernelHopfIdeal: the generated-over-A carrier is a closed subgroup of the transported integral carrier.
• kostantToralBaseChangePresentationIdeal_eq_generated_of_definingIdeal_eq: equal integral toral and root-generated defining ideals give equal transported presentations.
• kostantToralBaseChangePresentationIsoOfEq, kostantRootSubgroupToralCoordinateMapOfEq and kostantWeightTorusToralCoordinateMapOfEq: the same identification and integral generator maps, read through a named spelling J of the integral defining ideal. A carrier that names its own defining ideal specializes these rather than replaying the equality transport.
• hopfSpec_map_kostantRootSubgroupToralCoordinateMapOfEq_op and hopfSpec_map_kostantWeightTorusToralCoordinateMapOfEq_op: those integral generator maps represent the carrier's root-subgroup and weight-torus morphisms.
• pointsMulEquiv_kostantRootSubgroupToralCoordinateMapOfEq and pointsMulEquiv_kostantWeightTorusToralCoordinateMapOfEq: the corresponding integral maps on points are the represented root-subgroup and weight-torus matrices.
• pointsMulEquiv_kostantRootSubgroupToralBaseChangeCoordinateMap and pointsMulEquiv_kostantWeightTorusToralBaseChangeCoordinateMap: the transported maps preserve those matrices after base change.

References

This is the base-change compatibility of the explicit 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 TauCetiRoadmap/ReductiveGroups/README.md. The resulting carrier over the prime field and its algebraic closure is consumed by milestone L0 of the CFSGStatement roadmap.

The formal inputs are Tau Ceti's own coordinate base-change isomorphisms GeneralLinear.coordinateHopfAlgebraBaseChangeIso, AdditiveGroup.coordinateHopfAlgebraBaseChangeIso, and DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso, together with the Hopf-ideal quotient API of CommHopfAlgCat and the sibling Kostant/RootSubgroup/Scheme/ToralClosure/BaseChange.lean, whose declaration structure this file mirrors. The generic point-transport lemmas generalize the arguments in TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.BaseChange. Mathlib supplies the lower-level inputs those isomorphisms rest on (MvPolynomial.algebraTensorAlgEquiv, IsLocalization.Away.tensorProductEquivTMulRight, MonoidAlgebra.scalarTensorEquiv) and the category CommHopfAlgCat itself.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal {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 ↑(GeneralLinear.coordinateHopfAlgebra A n)

The Hopf ideal of O(GLₙ/A) presenting the base change of the toral Kostant closure: the inverse image of the base-changed defining ideal under the general-linear coordinate base-change isomorphism.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantToralBaseChangePresentationIdeal_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 → κ → ℤ) (A : Type u_1) [CommRing A] {x : ↑(GeneralLinear.coordinateHopfAlgebra A n)} : x ∈ kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A n).inv) x ∈ kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A

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

theorem TauCeti.UniversalEnvelopingAlgebra.map_tmul_mem_kostantToralBaseChangePresentationIdeal_of_mem {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] (s : A) {y : ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)} (hy : y ∈ kostantToralDefiningIdeal e h ρ M hM hnil b wt) : (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A n).hom) (s ⊗ₜ[ℤ] y) ∈ kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A

Transporting a pure tensor of a scalar and an integral defining equation produces an equation in the defining ideal over A.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIso {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 (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt))

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

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantToralBaseChangePresentationIso_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 (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A)) (kostantToralBaseChangePresentationIso e h ρ M hM hnil b wt A).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A n).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)))

The base-change identification of the toral carrier is compatible with the quotient maps.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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_1) [CommRing A] (i : I) : GeneralLinear.coordinateHopfAlgebra A n ⟶ AdditiveGroup.coordinateHopfAlgebra A

The base change of the ith integral root-subgroup coordinate map, transported into the coordinate Hopf algebras built directly over A.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap_def {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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_1) [CommRing A] (i : I) : kostantRootSubgroupBaseChangePresentationCoordinateMap e h ρ M hM hnil b A i = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A n).inv (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)) (AdditiveGroup.coordinateHopfAlgebraBaseChangeIso ℤ A).hom)

The transported base-changed root-subgroup map is the stated composite of the two coordinate base-change isomorphisms with the scalar extension of the map over ℤ.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralBaseChangePresentationCoordinateMap {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 (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

The transported base change of the ith root-subgroup coordinate map, factored through the transported toral carrier.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantRootSubgroupToralBaseChangePresentationCoordinateMap {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 (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A)) (kostantRootSubgroupToralBaseChangePresentationCoordinateMap e h ρ M hM hnil b wt A i) = kostantRootSubgroupBaseChangePresentationCoordinateMap e h ρ M hM hnil b A i

The factored root-subgroup map recovers the transported base change of the ith integral root-subgroup coordinate map.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusToralBaseChangePresentationCoordinateMap {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 (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup κ)).obj

The transported base change of the weight-torus coordinate map, factored through the transported toral carrier.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantWeightTorusToralBaseChangePresentationCoordinateMap {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 (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A)) (kostantWeightTorusToralBaseChangePresentationCoordinateMap e h ρ M hM hnil b wt A) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A wt

The factored weight-torus map recovers GeneralLinear.weightTorusBaseChangeCoordinateMap.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal_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) : (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (kostantRootSubgroupBaseChangePresentationCoordinateMap e h ρ M hM hnil b A i))).toRingHom

Every transported root-subgroup map kills the defining ideal over A.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal_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] : (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A wt))).toRingHom

The transported weight-torus map kills the defining ideal over A.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal_le_commonKernelHopfIdeal {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] : let K := fun (x : I ⊕ Unit) => match x with | Sum.inl val => AdditiveGroup.coordinateHopfAlgebra A | Sum.inr val => (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup κ)).obj; kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A ≤ CommHopfAlgCat.commonKernelHopfIdeal fun (j : I ⊕ Unit) => match j with | Sum.inl i => kostantRootSubgroupBaseChangePresentationCoordinateMap e h ρ M hM hnil b A i | Sum.inr val => GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A wt

The closed subgroup of GLₙ/A generated by the transported root subgroups and split torus lies in the transported base change of the integral toral carrier.

The reverse inclusion is deliberately not claimed: a Hopf ideal killed by all generators after base change need not descend to an integral Hopf ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal_eq_generated_of_definingIdeal_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 → κ → ℤ) (A : Type u_1) [CommRing A] (hideal : kostantToralDefiningIdeal e h ρ M hM hnil b wt = kostantGeneratedDefiningIdeal e h ρ M hM hnil b) : kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A = kostantGeneratedGeneralLinearBaseChangeIdeal e h ρ M hM hnil b A

Equality of the integral toral and root-generated defining ideals makes the transported toral and root-generated presentations in O(GLₙ/A) equal, for every commutative ring A. This does not identify them with the common kernel of the root-subgroup maps formed anew over A.

Transport along a named spelling of the integral defining ideal

A carrier constructed as a toral Kostant closure names its own integral defining ideal J and records the equality J = kostantToralDefiningIdeal e h ρ M hM hnil b wt. The declarations below re-express the base-change presentation and the two integral generator maps in terms of J, so a specialization does not replay the equality transport itself.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIsoOfEq {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] {J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)} (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) J)

The base-change identification of the toral carrier, with the integral quotient expressed using a named spelling J of the defining ideal.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantToralBaseChangePresentationIsoOfEq_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] {J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)} (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A)) (kostantToralBaseChangePresentationIsoOfEq e h ρ M hM hnil b wt A hJ).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A n).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) J))

The transported identification is compatible with the quotient maps.

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

The integral ith root-subgroup coordinate map, with source expressed using a named spelling J of the defining ideal.

Equations

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

@[simp]

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

The transported factored root-subgroup map recovers the represented root-subgroup coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_kostantRootSubgroupToralCoordinateMapOfEq {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)} (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) (i : I) (B : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points B)) : (GeneralLinear.pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra ℤ n) J B)) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (kostantRootSubgroupToralCoordinateMapOfEq e h ρ M hM hnil b wt hJ i)).app B)) q)) = (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) (AdditiveGroup.gaPointsMulEquiv.symm (AdditiveGroup.gaPointsMulEquiv q))

On points, the integral root-subgroup map factored through a named spelling of the toral carrier has the original divided-power exponential matrix.

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

The integral weight-torus coordinate map, with source expressed using a named spelling J of the defining ideal.

Equations

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

@[simp]

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

The transported factored weight-torus map recovers the weight-torus coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_kostantWeightTorusToralCoordinateMapOfEq {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)} [Fintype κ] (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) (B : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points B)) : (GeneralLinear.pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra ℤ n) J B)) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (kostantWeightTorusToralCoordinateMapOfEq e h ρ M hM hnil b wt hJ)).app B)) q)) = (kostantTorusMatrix M b wt) (SplitTorus.pointsMulEquiv q)

On points, the integral weight-torus map factored through a named spelling of the toral carrier is the diagonal matrix obtained by evaluating its weights.

theorem TauCeti.UniversalEnvelopingAlgebra.hopfSpec_map_kostantRootSubgroupToralCoordinateMapOfEq_op {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)} (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) (i : I) : (AlgebraicGeometry.hopfSpec ↧ℤ).map (kostantRootSubgroupToralCoordinateMapOfEq e h ρ M hM hnil b wt hJ i).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (kostantRootSubgroupToToral e h ρ M hM hnil b wt i) (CategoryTheory.eqToHom ⋯))

The spectrum of the integral factored ith root-subgroup coordinate map is the represented root-subgroup morphism into the toral carrier, transported to the named spelling J.

theorem TauCeti.UniversalEnvelopingAlgebra.hopfSpec_map_kostantWeightTorusToralCoordinateMapOfEq_op {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)} (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) : (AlgebraicGeometry.hopfSpec ↧ℤ).map (kostantWeightTorusToralCoordinateMapOfEq e h ρ M hM hnil b wt hJ).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (kostantWeightTorusToToral e h ρ M hM hnil b wt) (CategoryTheory.eqToHom ⋯))

The spectrum of the integral factored weight-torus coordinate map is the represented weight-torus morphism into the toral carrier, transported to the named spelling J.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIsoOfEq_hom_comp_rootSubgroupBaseChangeMap {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] {J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)} (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) (i : I) : CategoryTheory.CategoryStruct.comp (kostantToralBaseChangePresentationIsoOfEq e h ρ M hM hnil b wt A hJ).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (kostantRootSubgroupToralCoordinateMapOfEq e h ρ M hM hnil b wt hJ i)) (CommHopfAlgCat.ofHom ↑AdditiveGroup.gaScalarTensorBialgEquiv)) = kostantRootSubgroupToralBaseChangePresentationCoordinateMap e h ρ M hM hnil b wt A i

Under the transported identification, the factored ith root-subgroup map over A is the scalar extension of its integral coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_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] {J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)} (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) (i : I) (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : (GeneralLinear.pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A) B)) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (kostantRootSubgroupToralBaseChangePresentationCoordinateMap e h ρ M hM hnil b wt A i)).app B)) q)) = (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) (AdditiveGroup.gaPointsMulEquiv.symm (AdditiveGroup.gaPointsMulEquiv q))

On points, the transported factored root-subgroup map has the same divided-power exponential matrix as its integral source.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIsoOfEq_hom_comp_weightTorusBaseChangeMap {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] {J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)} (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) : CategoryTheory.CategoryStruct.comp (kostantToralBaseChangePresentationIsoOfEq e h ρ M hM hnil b wt A hJ).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (kostantWeightTorusToralCoordinateMapOfEq e h ρ M hM hnil b wt hJ)) (CommHopfAlgCat.ofHom ↑(MonoidAlgebra.scalarTensorBialgEquiv ℤ A))) = kostantWeightTorusToralBaseChangePresentationCoordinateMap e h ρ M hM hnil b wt A

Under the transported identification, the factored weight-torus map over A is the scalar extension of its integral coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_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] {J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)} [Fintype κ] (hJ : J = kostantToralDefiningIdeal e h ρ M hM hnil b wt) (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : (GeneralLinear.pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A n) (kostantToralBaseChangePresentationIdeal e h ρ M hM hnil b wt A) B)) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (kostantWeightTorusToralBaseChangePresentationCoordinateMap e h ρ M hM hnil b wt A)).app B)) q)) = (kostantTorusMatrix M b wt) (SplitTorus.pointsMulEquiv q)

On points, the transported factored weight-torus map is the diagonal matrix obtained by evaluating the integral weights.