Base change of a Kostant torus subsystem #
A Kostant torus subsystem over ℤ is the closed subgroup scheme of GLₙ generated by a selected
set of represented root subgroups together with the represented weight torus. This file transports
its coordinate presentation along ℤ → A. The base-changed defining ideal cuts out the specialized
carrier, and its quotient coordinate Hopf algebra is canonically the scalar extension of the
integral subsystem carrier.
The selected root-subgroup maps and the weight-torus map are transported through the same quotient
comparison. Their factorization equations ensure that scalar extension preserves the chosen
pinning data, rather than only the underlying carrier. The construction remains in tensor-product
coordinate algebras; transporting it into the coordinate rings constructed directly over A is a
separate comparison.
Main declarations #
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIdeal: the scalar extension of the integral subsystem ideal.TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIso: the quotient comparison identifying the specialized carrier with the base change of the integral carrier.TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupTorusSubsystemBaseChangeCoordinateMap: the transported factorization of each selected root subgroup.TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusTorusSubsystemBaseChangeCoordinateMap: the transported factorization of the weight torus.
References #
- R. W. Carter, Simple Groups of Lie Type, §4.4.
- B. Conrad, Reductive Group Schemes, §1.
The declaration structure follows the base-change interface for the full Kostant toral closure in
TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.ToralClosure.BaseChange.
noncomputable def
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIdeal
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
:
The defining ideal of the base-changed Kostant torus subsystem.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIdeal_def
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
:
kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt S hnilS A = CommHopfAlgCat.baseChangeHopfIdeal (kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS)
The subsystem base-change ideal is the scalar extension of its integral defining ideal.
noncomputable def
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIso
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
:
CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))
(kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt S hnilS A) ≅ CommHopfAlgCat.baseChange
(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n)
(kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS))
Quotienting by the specialized subsystem ideal agrees with base-changing the integral subsystem coordinate ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantTorusSubsystemBaseChangeIso_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)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
:
CategoryTheory.CategoryStruct.comp
(CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))
(kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt S hnilS A))
(kostantTorusSubsystemBaseChangeIso e h ρ M hM b wt S hnilS A).hom = CommHopfAlgCat.baseChangeMap
(CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n)
(kostantTorusSubsystemDefiningIdeal e h ρ M hM b wt S hnilS))
The subsystem base-change comparison is compatible with the integral quotient map.
noncomputable def
TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupTorusSubsystemBaseChangeCoordinateMap
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
{i : I}
(hi : i ∈ S)
:
The factored coordinate map of a selected root subgroup after base change.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantRootSubgroupTorusSubsystemBaseChangeCoordinateMap
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
{i : I}
(hi : i ∈ S)
:
CategoryTheory.CategoryStruct.comp
(CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))
(kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt S hnilS A))
(kostantRootSubgroupTorusSubsystemBaseChangeCoordinateMap e h ρ M hM b wt S hnilS A hi) = CommHopfAlgCat.baseChangeMap (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)
The specialized quotient map followed by a selected root-subgroup map is the base change of the corresponding integral root-subgroup coordinate map.
noncomputable def
TauCeti.UniversalEnvelopingAlgebra.kostantWeightTorusTorusSubsystemBaseChangeCoordinateMap
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
:
The factored coordinate map of the represented weight torus after base change.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantWeightTorusTorusSubsystemBaseChangeCoordinateMap
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
:
CategoryTheory.CategoryStruct.comp
(CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))
(kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt S hnilS A))
(kostantWeightTorusTorusSubsystemBaseChangeCoordinateMap e h ρ M hM b wt S hnilS A) = CommHopfAlgCat.baseChangeMap (GeneralLinear.weightTorusCoordinateMap wt)
The specialized quotient map followed by the weight-torus map is the base change of the integral weight-torus coordinate map.
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIdeal_toIdeal_le_root_ker
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
{i : I}
(hi : i ∈ S)
:
(kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt S hnilS A).toIdeal ≤ RingHom.ker
(↑(CommHopfAlgCat.Hom.hom
(CommHopfAlgCat.baseChangeMap (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b)))).toRingHom
Every selected base-changed root-subgroup map kills the specialized subsystem ideal.
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeIdeal_toIdeal_le_torus_ker
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(S : Set I)
(hnilS : ∀ (i : ↑S), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i))))
(A : Type u_1)
[CommRing A]
:
(kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt S hnilS A).toIdeal ≤ RingHom.ker
(↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.baseChangeMap (GeneralLinear.weightTorusCoordinateMap wt)))).toRingHom
The base-changed weight-torus map kills the specialized subsystem ideal.
Inclusion into the full toral closure #
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantToralBaseChangeIdeal_le_kostantTorusSubsystemBaseChangeIdeal
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(A : Type u_1)
[CommRing A]
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(T : Set I)
:
kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A ≤ kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt T ⋯ A
Base change preserves the inclusion of the full toral defining ideal in every subsystem defining ideal.
noncomputable def
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeInclusionCoordinateMap
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(A : Type u_1)
[CommRing A]
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(T : Set I)
:
CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))
(kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A) ⟶ CommHopfAlgCat.quotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))
(kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt T ⋯ A)
The coordinate morphism of the base-changed inclusion of a torus subsystem into the full toral closure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantTorusSubsystemBaseChangeInclusionCoordinateMap
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(A : Type u_1)
[CommRing A]
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(T : Set I)
:
CategoryTheory.CategoryStruct.comp
(CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))
(kostantToralBaseChangeIdeal e h ρ M hM hnil b wt A))
(kostantTorusSubsystemBaseChangeInclusionCoordinateMap e h ρ M hM b wt A hnil T) = CommHopfAlgCat.mkQuotient (CommHopfAlgCat.baseChange (GeneralLinear.coordinateHopfAlgebra ℤ n))
(kostantTorusSubsystemBaseChangeIdeal e h ρ M hM b wt T ⋯ A)
The base-changed subsystem inclusion is compatible with the two quotient maps.
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeInclusionCoordinateMap_surjective
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(A : Type u_1)
[CommRing A]
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(T : Set I)
:
Function.Surjective
⇑(CommHopfAlgCat.Hom.hom (kostantTorusSubsystemBaseChangeInclusionCoordinateMap e h ρ M hM b wt A hnil T))
The coordinate morphism of a base-changed torus-subsystem inclusion is surjective.
@[simp]
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeInclusionCoordinateMap_comp_root
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(A : Type u_1)
[CommRing A]
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(T : Set I)
{i : I}
(hi : i ∈ T)
:
CategoryTheory.CategoryStruct.comp (kostantTorusSubsystemBaseChangeInclusionCoordinateMap e h ρ M hM b wt A hnil T)
(kostantRootSubgroupTorusSubsystemBaseChangeCoordinateMap e h ρ M hM b wt T ⋯ A hi) = kostantRootSubgroupToralBaseChangeCoordinateMap e h ρ M hM hnil b wt A i
The base-changed subsystem inclusion intertwines each selected root-subgroup map with its factorization through the full toral closure.
@[simp]
theorem
TauCeti.UniversalEnvelopingAlgebra.kostantTorusSubsystemBaseChangeInclusionCoordinateMap_comp_weightTorus
{L : Type u}
[LieRing L]
[LieAlgebra ℚ L]
{I : Type w}
{κ : Type}
[Finite κ]
{V : Type}
[AddCommGroup V]
[Module ℚ V]
(e : I → L)
(h : κ → L)
(ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V)
(M : AddSubgroup V)
(hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M)
{n : ℕ}
(b : Module.Basis (Fin n) ℤ ↥M)
(wt : Fin n → κ → ℤ)
(A : Type u_1)
[CommRing A]
(hnil : ∀ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
(T : Set I)
:
CategoryTheory.CategoryStruct.comp (kostantTorusSubsystemBaseChangeInclusionCoordinateMap e h ρ M hM b wt A hnil T)
(kostantWeightTorusTorusSubsystemBaseChangeCoordinateMap e h ρ M hM b wt T ⋯ A) = kostantWeightTorusToralBaseChangeCoordinateMap e h ρ M hM hnil b wt A
The base-changed subsystem inclusion intertwines the represented weight-torus maps.