Integral orbits of a Kostant form

Let L be a Lie algebra over ℚ and let U_ℤ = kostantForm e h be the Kostant integral form generated by families e of root vectors and h of Cartan vectors. For a module V over U(L) and a vector v : V, this file studies the integral orbit

U_ℤ • v ⊆ V.

The orbit is stable under U_ℤ; in particular, it is preserved by the divided powers of the root vectors and the binomial coefficients of the Cartan vectors. When e and h generate L as a Lie algebra, its ℚ-span is the whole U(L)-submodule generated by v. For a cyclic module this is all of V.

Finite generation over ℤ is not proved here. Thus the orbit is not yet asserted to be a lattice in the sense of Humphreys §27; that requires the integral Poincaré--Birkhoff--Witt theorem. The present stability and spanning results are the parts of the admissible-lattice construction that are available without integral PBW.

The representation-oriented variant orbitOfRep starts from a subring S, an algebra representation ρ : A →ₐ[ℚ] End(V), and a set of generating vectors. It is the integral span of all their images under S. This avoids manufacturing a global A-module instance when a construction already carries its representation as an algebra homomorphism. Its specialization to the Kostant form and a singleton agrees with kostantOrbit.

Main definitions and results

• TauCeti.UniversalEnvelopingAlgebra.kostantOrbit: the integral orbit U_ℤ • v.
• TauCeti.UniversalEnvelopingAlgebra.smul_mem_kostantOrbit: stability under the integral form.
• TauCeti.UniversalEnvelopingAlgebra.dividedPower_smul_mem_kostantOrbit and TauCeti.UniversalEnvelopingAlgebra.ringChoose_smul_mem_kostantOrbit: stability under the two families of Kostant generators.
• TauCeti.UniversalEnvelopingAlgebra.span_kostantOrbit_eq_span_singleton: under a Lie-generation hypothesis, the ℚ-span is the U(L)-submodule generated by v.
• TauCeti.UniversalEnvelopingAlgebra.span_kostantOrbit_eq_top: for a cyclic module the orbit spans V over ℚ.
• TauCeti.UniversalEnvelopingAlgebra.orbitOfRep: the integral orbit of a set through an algebra representation, with stability and spanning lemmas.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26 and §27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• R. Steinberg, Lectures on Chevalley Groups, §2.

def TauCeti.UniversalEnvelopingAlgebra.kostantOrbit {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] (e : ι → L) (h : κ → L) (v : V) : Submodule ℤ V

The integral orbit generated by v under the Kostant form attached to e and h.

This is the span of v over the subring kostantForm e h, regarded as a ℤ-submodule of V. No finite-generation or lattice property is asserted.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantOrbit e h v = Submodule.restrictScalars ℤ (↥(TauCeti.UniversalEnvelopingAlgebra.kostantForm e h) ∙ v)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantOrbit_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] {e : ι → L} {h : κ → L} {v x : V} : x ∈ kostantOrbit e h v ↔ ∃ u ∈ kostantForm e h, u • v = x

The Kostant orbit consists exactly of the vectors u • v for u in the integral form.

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantOrbit_self {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] {e : ι → L} {h : κ → L} {v : V} : v ∈ kostantOrbit e h v

The generating vector belongs to its Kostant orbit.

theorem TauCeti.UniversalEnvelopingAlgebra.smul_mem_kostantOrbit {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] {e : ι → L} {h : κ → L} {v : V} {u : UniversalEnvelopingAlgebra ℚ L} (hu : u ∈ kostantForm e h) {x : V} (hx : x ∈ kostantOrbit e h v) : u • x ∈ kostantOrbit e h v

The Kostant orbit is stable under the integral form.

theorem TauCeti.UniversalEnvelopingAlgebra.dividedPower_smul_mem_kostantOrbit {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] {e : ι → L} {h : κ → L} {v : V} (i : ι) (n : ℕ) {x : V} (hx : x ∈ kostantOrbit e h v) : Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) • x ∈ kostantOrbit e h v

The divided powers of the root vectors preserve the Kostant orbit. This is the stability statement needed before locally finite root-vector exponentials can be defined.

theorem TauCeti.UniversalEnvelopingAlgebra.ringChoose_smul_mem_kostantOrbit {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] {e : ι → L} {h : κ → L} {v : V} (i : κ) (n : ℕ) {x : V} (hx : x ∈ kostantOrbit e h v) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n • x ∈ kostantOrbit e h v

The binomial coefficients of the Cartan vectors preserve the Kostant orbit.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantOrbit_one {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) : kostantOrbit e h 1 = AddSubgroup.toIntSubmodule (kostantForm e h).toAddSubgroup

The Kostant orbit of the identity in the regular module is the integral form itself.

theorem TauCeti.UniversalEnvelopingAlgebra.span_kostantOrbit_eq_span_singleton {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] [Module ℚ V] [IsScalarTower ℚ (UniversalEnvelopingAlgebra ℚ L) V] (e : ι → L) (h : κ → L) (hgen : LieSubalgebra.lieSpan ℚ L (Set.range e ∪ Set.range h) = ⊤) (v : V) : Submodule.span ℚ ↑(kostantOrbit e h v) = Submodule.restrictScalars ℚ (UniversalEnvelopingAlgebra ℚ L ∙ v)

If the supplied root and Cartan vectors generate L as a Lie algebra, the ℚ-span of their Kostant orbit is the U(L)-submodule generated by v.

theorem TauCeti.UniversalEnvelopingAlgebra.span_kostantOrbit_eq_top {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] [Module ℚ V] [IsScalarTower ℚ (UniversalEnvelopingAlgebra ℚ L) V] (e : ι → L) (h : κ → L) (hgen : LieSubalgebra.lieSpan ℚ L (Set.range e ∪ Set.range h) = ⊤) (v : V) (hv : UniversalEnvelopingAlgebra ℚ L ∙ v = ⊤) : Submodule.span ℚ ↑(kostantOrbit e h v) = ⊤

If v generates V over U(L), the Kostant orbit spans the whole module over ℚ.

def TauCeti.UniversalEnvelopingAlgebra.orbitOfRep {A : Type u} [Ring A] [Algebra ℚ A] {V : Type v} [AddCommGroup V] [Module ℚ V] (S : Subring A) (ρ : A →ₐ[ℚ] Module.End ℚ V) (X : Set V) : Submodule ℤ V

The integral orbit of a set through an algebra representation: the ℤ-span of all ρ a x with a ∈ S and x ∈ X.

Equations

• TauCeti.UniversalEnvelopingAlgebra.orbitOfRep S ρ X = Submodule.span ℤ {v : V | ∃ a ∈ S, ∃ x ∈ X, (ρ a) x = v}

theorem TauCeti.UniversalEnvelopingAlgebra.orbitOfRep_def {A : Type u} [Ring A] [Algebra ℚ A] {V : Type v} [AddCommGroup V] [Module ℚ V] (S : Subring A) (ρ : A →ₐ[ℚ] Module.End ℚ V) (X : Set V) : orbitOfRep S ρ X = Submodule.span ℤ {v : V | ∃ a ∈ S, ∃ x ∈ X, (ρ a) x = v}

The represented orbit is the integral span of the images of its generators.

theorem TauCeti.UniversalEnvelopingAlgebra.apply_mem_orbitOfRep {A : Type u} [Ring A] [Algebra ℚ A] {V : Type v} [AddCommGroup V] [Module ℚ V] (S : Subring A) (ρ : A →ₐ[ℚ] Module.End ℚ V) (X : Set V) {a : A} (ha : a ∈ S) {x : V} (hx : x ∈ X) : (ρ a) x ∈ orbitOfRep S ρ X

A represented translate of a generator belongs to its integral orbit.

theorem TauCeti.UniversalEnvelopingAlgebra.subset_orbitOfRep {A : Type u} [Ring A] [Algebra ℚ A] {V : Type v} [AddCommGroup V] [Module ℚ V] (S : Subring A) (ρ : A →ₐ[ℚ] Module.End ℚ V) (X : Set V) : X ⊆ ↑(orbitOfRep S ρ X)

The generators themselves belong to their integral orbit.

theorem TauCeti.UniversalEnvelopingAlgebra.orbitOfRep_le_iff {A : Type u} [Ring A] [Algebra ℚ A] {V : Type v} [AddCommGroup V] [Module ℚ V] (S : Subring A) (ρ : A →ₐ[ℚ] Module.End ℚ V) (X : Set V) (N : Submodule ℤ V) : orbitOfRep S ρ X ≤ N ↔ ∀ a ∈ S, ∀ x ∈ X, (ρ a) x ∈ N

The elimination principle for a represented integral orbit.

theorem TauCeti.UniversalEnvelopingAlgebra.apply_mem_orbitOfRep_of_mem {A : Type u} [Ring A] [Algebra ℚ A] {V : Type v} [AddCommGroup V] [Module ℚ V] (S : Subring A) (ρ : A →ₐ[ℚ] Module.End ℚ V) (X : Set V) {a : A} (ha : a ∈ S) {v : V} (hv : v ∈ orbitOfRep S ρ X) : (ρ a) v ∈ orbitOfRep S ρ X

The represented integral orbit is stable under the subring.

theorem TauCeti.UniversalEnvelopingAlgebra.span_orbitOfRep_eq_span {A : Type u} [Ring A] [Algebra ℚ A] {V : Type v} [AddCommGroup V] [Module ℚ V] (S : Subring A) (ρ : A →ₐ[ℚ] Module.End ℚ V) (X : Set V) (hS : Submodule.span ℚ ↑S = ⊤) : Submodule.span ℚ ↑(orbitOfRep S ρ X) = Submodule.span ℚ {v : V | ∃ (a : A), ∃ x ∈ X, (ρ a) x = v}

If S spans A over ℚ, the rational span of the represented integral orbit is the span of all translates through the full algebra.

theorem TauCeti.UniversalEnvelopingAlgebra.span_orbitOfRep_eq_top {A : Type u} [Ring A] [Algebra ℚ A] {V : Type v} [AddCommGroup V] [Module ℚ V] (S : Subring A) (ρ : A →ₐ[ℚ] Module.End ℚ V) (X : Set V) (hX : Submodule.span ℚ X = ⊤) : Submodule.span ℚ ↑(orbitOfRep S ρ X) = ⊤

If the supplied vectors span over ℚ, their represented integral orbit is full.

theorem TauCeti.UniversalEnvelopingAlgebra.orbitOfRep_kostantForm_singleton_eq_kostantOrbit {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module (UniversalEnvelopingAlgebra ℚ L) V] [Module ℚ V] [IsScalarTower ℚ (UniversalEnvelopingAlgebra ℚ L) V] (e : ι → L) (h : κ → L) (v : V) : orbitOfRep (kostantForm e h) (Algebra.lsmul ℚ ℚ V) {v} = kostantOrbit e h v

The represented orbit of a singleton under a Kostant form agrees with kostantOrbit.