Birkhoff's faithful nilpotent representation

A positively weighted ordered Lie basis gives a left-multiplication action on the weighted PBW quotient at cutoff N. Every acting operator has N-th power zero, and the action is faithful when N exceeds every basis weight. A finite basis gives a module-finite carrier. Lower-central weights supply these conditions for every finite-dimensional nilpotent Lie algebra, over a field of any characteristic.

The action reuses LieHom.leftRegularRep. The carrier, its finiteness, separation of the Lie generators, and their uniform power bound come from the weighted PBW construction in TauCeti.Algebra.Lie.UniversalEnveloping.PBW.Weighted.Basic. No Lie-module instance is installed on the quotient: consumers use the explicit Lie homomorphism.

References

• N. Jacobson, Lie Algebras, Chapter V, Birkhoff's theorem.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §17.

noncomputable def Module.Basis.weightedPBWRepresentation {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (hbracket : ∀ (i j k : ι), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0) (N : ℕ) : L →ₗ⁅R⁆ End R (UniversalEnvelopingAlgebra R L ⧸ b.weightedPBWIdeal w hbracket N)

Left multiplication by Lie generators on the weighted PBW quotient at cutoff N.

theorem Module.Basis.weightedPBWRepresentation_def {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (hbracket : ∀ (i j k : ι), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0) (N : ℕ) : b.weightedPBWRepresentation w hbracket N = ((Ideal.Quotient.mkₐ R (b.weightedPBWIdeal w hbracket N)).toLieHom.comp (UniversalEnvelopingAlgebra.ι R)).leftRegularRep

The weighted action is the left-regular representation of the canonical quotient map.

@[simp]

theorem Module.Basis.weightedPBWRepresentation_apply {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (hbracket : ∀ (i j k : ι), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0) (N : ℕ) (x : L) (a : UniversalEnvelopingAlgebra R L ⧸ b.weightedPBWIdeal w hbracket N) : ((b.weightedPBWRepresentation w hbracket N) x) a = (Ideal.Quotient.mk (b.weightedPBWIdeal w hbracket N)) ((UniversalEnvelopingAlgebra.ι R) x) * a

The weighted action multiplies by the quotient class of the canonical Lie generator.

theorem Module.Basis.weightedPBWRepresentation_apply_mk {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (hbracket : ∀ (i j k : ι), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0) (N : ℕ) (x : L) (a : UniversalEnvelopingAlgebra R L) : ((b.weightedPBWRepresentation w hbracket N) x) ((Ideal.Quotient.mk (b.weightedPBWIdeal w hbracket N)) a) = (Ideal.Quotient.mk (b.weightedPBWIdeal w hbracket N)) ((UniversalEnvelopingAlgebra.ι R) x * a)

Acting on a representative multiplies by the Lie generator before taking its quotient class.

theorem Module.Basis.weightedPBWRepresentation_eq_zero_iff {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (hbracket : ∀ (i j k : ι), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0) (N : ℕ) (x : L) : (b.weightedPBWRepresentation w hbracket N) x = 0 ↔ (UniversalEnvelopingAlgebra.ι R) x ∈ b.weightedPBWIdeal w hbracket N

A Lie element acts by zero precisely when its canonical image lies in the weighted ideal.

theorem Module.Basis.weightedPBWRepresentation_injective {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (hbracket : ∀ (i j k : ι), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0) (N : ℕ) (hN : ∀ (i : ι), w i < N) : Function.Injective ⇑(b.weightedPBWRepresentation w hbracket N)

The weighted action is faithful when the cutoff exceeds every basis weight.

@[simp]

theorem Module.Basis.weightedPBWRepresentation_pow_eq_zero {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (hbracket : ∀ (i j k : ι), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0) (hpos : ∀ (i : ι), 0 < w i) (N : ℕ) (x : L) : (b.weightedPBWRepresentation w hbracket N) x ^ N = 0

With positive weights, every acting operator has N-th power zero, uniformly in the Lie element. No nilpotence, finiteness, or field assumption is needed for this bound.

theorem TauCeti.exists_faithful_weightedPBWRepresentation (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieRing.IsNilpotent L] : ∃ (N : ℕ) (b : Module.Basis (Fin (Module.finrank K L)) K L) (w : Fin (Module.finrank K L) → ℕ) (hbracket : ∀ (i j k : Fin (Module.finrank K L)), w k < w i + w j → (b.repr ⁅b i, b j⁆) k = 0), 0 < N ∧ (∀ (i : Fin (Module.finrank K L)), 0 < w i ∧ w i < N) ∧ Module.Finite K (UniversalEnvelopingAlgebra K L ⧸ b.weightedPBWIdeal w hbracket N) ∧ Function.Injective ⇑(b.weightedPBWRepresentation w hbracket N) ∧ ∀ (x : L), (b.weightedPBWRepresentation w hbracket N) x ^ N = 0

Birkhoff's theorem on a weighted PBW quotient. A finite-dimensional nilpotent Lie algebra has a faithful left-multiplication representation on a finite-dimensional weighted enveloping quotient, with one positive nilpotence bound for all acting operators. The basis, weights, and cutoff are supplied by the conclusion, in every characteristic.