Papers With

← All papers
First page of Dimension subrings of Lie rings

Dimension subrings of Lie rings

Vasily Ionin, Roman Mikhailov, Tima Petrov

math.GR Oct 1, 2026 · v1 math.RA
formalization algebra
Read PDF arXiv abstract Code
TL;DR
The main theorems on Lie ring dimension subrings, including the integral PBW theorem, are formalized in Lean 4 with no sorry placeholders or added axioms.
Abstract
We show that, unlike the lower central series, the dimension series of a Lie ring need not stabilize when two consecutive terms coincide; in fact, arbitrarily long finite plateaux occur. We prove that $D_n(L)/γ_{n+1}(L)$ is central in $L/γ_{n+1}(L)$ for every $n\geq1$, in contrast to the group case. If $c\geq2$ and $L$ is metabelian and nilpotent of class at most $c$, we prove that $D_{2c-1}(L)=0$. In particular, our results imply that $D_5(L)\subseteqγ_4(L)$ for every Lie ring $L$.
Problem

The dimension series D_n(L) of a Lie ring is defined from the powers of the augmentation ideal of its universal enveloping algebra. It need not equal the lower central series, and how the two series differ is poorly understood.

Approach

The authors build explicit metabelian Lie rings L_N by presentations to exhibit plateaux in the dimension series. They prove centrality of D_n(L)/γ_{n+1}(L) using the adjoint U(L)-module structure on ideals. For vanishing results they develop a certificate criterion based on central extensions and additive retractions of U(T). Most results, including the integral PBW theorem, are formalized in Lean 4, with the formalization generated with AI assistance.

Results

The dimension series can have arbitrarily long finite plateaux. D_n(L)/γ_{n+1}(L) is central in L/γ_{n+1}(L) for every n≥1, and D_{2c-1}(L)=0 for metabelian Lie rings L of nilpotency class at most c, where c≥2. Consequently D_5(L)⊆γ_4(L) for every Lie ring L. Theorems A, B and C are machine-checked in Lean 4 with no sorry placeholders.