Weighted PBW truncation

Given an ordered Lie basis with natural weights, the span of its PBW monomials of weight at least N is characterized by the vanishing of all coordinates below N. If brackets do not lower the sum of the input weights, straightening preserves this lower bound. Consequently these spans form a multiplicative descending filtration and are two-sided ideals.

Positive weights on a finite basis give finite-dimensional truncations. Lower-central weights on a nilpotent Lie algebra supply the bracket condition in every characteristic. These quotients provide finite associative targets for faithful nilpotent representations.

The construction uses Module.Basis.pbwBasis and TauCeti.exists_basis_weight_lowerCentralSeries. Finiteness follows from Finsupp.finite_of_nat_weight_lt, without assuming a field in the basis-level results.

References

• N. Jacobson, Lie Algebras, Interscience (1962), Chapter V.

noncomputable def Module.Basis.weightedPBWFiltration {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (N : ℕ) : Submodule R (UniversalEnvelopingAlgebra R L)

The descending weighted PBW filtration: the span of monomials of weight at least N.

theorem Module.Basis.weightedPBWFiltration_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 : ι → ℕ) (N : ℕ) : b.weightedPBWFiltration w N = Submodule.span R (⇑b.pbwBasis '' {n : ι →₀ ℕ | N ≤ (Finsupp.weight w) n})

The weighted PBW filtration is the span of the monomials at or above the cutoff.

@[simp]

theorem Module.Basis.mem_weightedPBWFiltration_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 : ι → ℕ) (N : ℕ) (a : UniversalEnvelopingAlgebra R L) : a ∈ b.weightedPBWFiltration w N ↔ ∀ (n : ι →₀ ℕ), (Finsupp.weight w) n < N → (b.pbwBasis.repr a) n = 0

Membership is equivalent to vanishing of all PBW coefficients of weight below the cutoff.

theorem Module.Basis.pbwBasis_mem_weightedPBWFiltration {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) {N : ℕ} {n : ι →₀ ℕ} (hn : N ≤ (Finsupp.weight w) n) : b.pbwBasis n ∈ b.weightedPBWFiltration w N

A PBW basis vector of weight at least the cutoff belongs to the weighted filtration.

theorem Module.Basis.weightedPBWFiltration_antitone {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) : Antitone (b.weightedPBWFiltration w)

Increasing the cutoff decreases the weighted PBW filtration.

@[simp]

theorem Module.Basis.weightedPBWFiltration_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 : ι → ℕ) : b.weightedPBWFiltration w 0 = ⊤

At cutoff zero the weighted PBW filtration is the whole enveloping algebra.

theorem Module.Basis.pbwMonomial_mem_weightedPBWFiltration {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) (l : List ι) {N : ℕ} (hN : N ≤ (List.map w l).sum) : TauCeti.UniversalEnvelopingAlgebra.pbwMonomial R L (⇑b) l ∈ b.weightedPBWFiltration w N

Straightening an arbitrary basis word does not decrease its weight.

theorem Module.Basis.mul_mem_weightedPBWFiltration {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) {m n : ℕ} {a c : UniversalEnvelopingAlgebra R L} (ha : a ∈ b.weightedPBWFiltration w m) (hc : c ∈ b.weightedPBWFiltration w n) : a * c ∈ b.weightedPBWFiltration w (m + n)

Weights add under multiplication in the descending PBW filtration.

noncomputable def Module.Basis.weightedPBWIdeal {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 : ℕ) : Ideal (UniversalEnvelopingAlgebra R L)

The weighted truncation ideal, with underlying scalar submodule the weighted PBW span.

@[simp]

theorem Module.Basis.mem_weightedPBWIdeal_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 : ℕ) (a : UniversalEnvelopingAlgebra R L) : a ∈ b.weightedPBWIdeal w hbracket N ↔ a ∈ b.weightedPBWFiltration w N

Weighted truncation ideal membership is membership in the scalar PBW span.

theorem Module.Basis.weightedPBWIdeal_antitone {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) : Antitone (b.weightedPBWIdeal w hbracket)

Increasing the cutoff decreases the weighted PBW truncation ideal.

@[simp]

theorem Module.Basis.weightedPBWIdeal_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) : b.weightedPBWIdeal w hbracket 0 = ⊤

At cutoff zero the weighted PBW truncation ideal is the whole enveloping algebra.

instance Module.Basis.weightedPBWIdeal_isTwoSided {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.weightedPBWIdeal w hbracket N).IsTwoSided

The weighted PBW truncation ideal is two-sided: multiplication on the right also preserves the lower weight bound.

theorem Module.Basis.span_image_pbwBasis_quotient_weightedPBWIdeal {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 : ℕ) : Submodule.span R ((fun (n : ι →₀ ℕ) => (Ideal.Quotient.mk (b.weightedPBWIdeal w hbracket N)) (b.pbwBasis n)) '' {n : ι →₀ ℕ | (Finsupp.weight w) n < N}) = ⊤

The images of PBW monomials below the cutoff span the weighted quotient.

theorem Module.Basis.moduleFinite_quotient_weightedPBWIdeal {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) [Finite ι] (hpos : ∀ (i : ι), 0 < w i) (N : ℕ) : Module.Finite R (UniversalEnvelopingAlgebra R L ⧸ b.weightedPBWIdeal w hbracket N)

A finite Lie basis with positive weights gives a module-finite weighted quotient, over any commutative coefficient ring.

theorem Module.Basis.quotient_weightedPBWIdeal_ι_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 fun (x : L) => (Ideal.Quotient.mk (b.weightedPBWIdeal w hbracket N)) ((UniversalEnvelopingAlgebra.ι R) x)

If the cutoff exceeds every basis weight, the quotient remains injective on the canonical copy of the Lie algebra.

theorem Module.Basis.ι_mem_weightedPBWFiltration {R : Type u_1} {L : Type u_2} {ι : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LinearOrder ι] (b : Basis ι R L) (w : ι → ℕ) (x : L) {m : ℕ} (hx : ∀ i ∈ (b.repr x).support, m ≤ w i) : (UniversalEnvelopingAlgebra.ι R) x ∈ b.weightedPBWFiltration w m

A canonical Lie generator has weight at least m when all of its nonzero basis coordinates do.

theorem Module.Basis.pow_mem_weightedPBWFiltration {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) {a : UniversalEnvelopingAlgebra R L} {m : ℕ} (ha : a ∈ b.weightedPBWFiltration w m) (n : ℕ) : a ^ n ∈ b.weightedPBWFiltration w (n * m)

Powers multiply the lower weight bound.

theorem Module.Basis.quotient_weightedPBWIdeal_ι_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) : (Ideal.Quotient.mk (b.weightedPBWIdeal w hbracket N)) ((UniversalEnvelopingAlgebra.ι R) x) ^ N = 0

With positive weights, every Lie generator has its N-th power zero in the weighted quotient at cutoff N.

theorem TauCeti.UniversalEnvelopingAlgebra.exists_weightedPBWIdeal_of_isNilpotent (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 fun (x : L) => (Ideal.Quotient.mk (b.weightedPBWIdeal w hbracket N)) ((UniversalEnvelopingAlgebra.ι K) x)) ∧ ∀ (x : L), (Ideal.Quotient.mk (b.weightedPBWIdeal w hbracket N)) ((UniversalEnvelopingAlgebra.ι K) x) ^ N = 0

A finite-dimensional nilpotent Lie algebra admits a weighted PBW truncation which is finite-dimensional, preserves the canonical Lie generators injectively, and makes their powers vanish uniformly. The positive weights and positive cutoff are part of the conclusion.