Internal generator family for Kostant toral closures

This module contains the shared implementation of the coordinate-map family used to construct both the full Kostant toral closure and its selected-root subsystems. It is internal plumbing; public users should use the characterized defining ideals and factorization maps instead.

@[reducible, inline]

noncomputable abbrev TauCeti.UniversalEnvelopingAlgebra.ToralClosure.Internal.kostantToralGeneratorCodomain {J : Type v} {kappa : Type} [Finite kappa] (j : J ⊕ Unit) : CommHopfAlgCat ℤ

The coordinate Hopf algebra receiving a root-subgroup or weight-torus generator map.

Equations

• TauCeti.UniversalEnvelopingAlgebra.ToralClosure.Internal.kostantToralGeneratorCodomain (Sum.inl val) = TauCeti.AdditiveGroup.coordinateHopfAlgebra ℤ
• TauCeti.UniversalEnvelopingAlgebra.ToralClosure.Internal.kostantToralGeneratorCodomain (Sum.inr val) = (TauCeti.DiagonalizableGroup.coordinateRing ℤ (TauCeti.SplitTorus.characterGroup kappa)).obj

noncomputable def TauCeti.UniversalEnvelopingAlgebra.ToralClosure.Internal.kostantToralGeneratorMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {J : Type v} {kappa : Type} [Finite kappa] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : kappa → L) (rho : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (rho u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → kappa → ℤ) (r : J → I) (hnilJ : ∀ (j : J), IsNilpotent (rho ((UniversalEnvelopingAlgebra.ι ℚ) (e (r j))))) (j : J ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra ℤ n ⟶ kostantToralGeneratorCodomain j

The family consisting of reindexed root-subgroup coordinate maps and the weight-torus map.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.UniversalEnvelopingAlgebra.ToralClosure.Internal.kostantToralGeneratorMap e h rho M hM b wt r hnilJ (Sum.inr val) = TauCeti.GeneralLinear.weightTorusCoordinateMap wt

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.ToralClosure.Internal.kostantToralGeneratorMap_inl {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {J : Type v} {kappa : Type} [Finite kappa] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : kappa → L) (rho : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (rho u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → kappa → ℤ) (r : J → I) (hnilJ : ∀ (j : J), IsNilpotent (rho ((UniversalEnvelopingAlgebra.ι ℚ) (e (r j))))) (j : J) : kostantToralGeneratorMap e h rho M hM b wt r hnilJ (Sum.inl j) = kostantRootSubgroupCoordinateMap e h rho M hM (r j) ⋯ b

A root-indexed member of the internal generator family is its represented root-subgroup coordinate map.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.ToralClosure.Internal.kostantToralGeneratorMap_inr {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {J : Type v} {kappa : Type} [Finite kappa] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : kappa → L) (rho : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (rho u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → kappa → ℤ) (r : J → I) (hnilJ : ∀ (j : J), IsNilpotent (rho ((UniversalEnvelopingAlgebra.ι ℚ) (e (r j))))) : kostantToralGeneratorMap e h rho M hM b wt r hnilJ (Sum.inr ()) = GeneralLinear.weightTorusCoordinateMap wt

The final member of the internal generator family is the represented weight-torus coordinate map.

theorem TauCeti.UniversalEnvelopingAlgebra.ToralClosure.Internal.commonKernelHopfIdeal_kostantToralGeneratorMap_subtype {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {kappa : Type} [Finite kappa] {V : Type} [AddCommGroup V] [Module ℚ V] (e : I → L) (h : kappa → L) (rho : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (rho u) m ∈ M) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (wt : Fin n → kappa → ℤ) (S : Set I) (hnilS : ∀ (i : ↑S), IsNilpotent (rho ((UniversalEnvelopingAlgebra.ι ℚ) (e ↑i)))) : CommHopfAlgCat.commonKernelHopfIdeal (kostantToralGeneratorMap e h rho M hM b wt Subtype.val hnilS) = CommHopfAlgCat.commonKernelHopfIdeal fun (j : ↑S ⊕ Unit) => match j with | Sum.inl i => kostantRootSubgroupCoordinateMap e h rho M hM ↑i ⋯ b | Sum.inr val => GeneralLinear.weightTorusCoordinateMap wt

The common kernel of a subtype-indexed generator family can be written using its root and torus branches without exposing the implementation of the family itself.