Solution (source code)

= Solution

The correspondence concerns <uniform pro-p groups> and <powerful Lie lattices>, with their natural morphisms. Put $\epsilon=1$ for odd $p$ and $\epsilon=2$ for $p=2$. A <powerful pro-p group> is a <pro-p group> whose closed <commutator subgroup> lies in its closed $p^\epsilon$-power <subgroup>. It is uniform when it is topologically finitely generated and all successive indices in its <lower p-series> are equal. Equivalently, a finitely generated <powerful pro-p group> is uniform precisely when it is a <torsion-free group>. A <powerful Lie algebra over p-adic integers> means a <Lie algebra> over $\mathbb Z_p$ that is free of finite rank as a <module> and satisfies
$$
[L,L]\subseteq p^\epsilon L.
$$
Here a <Lie algebra> over a ring is a <module> with an alternating bilinear <Lie bracket> satisfying the <Jacobi identity>. Finite freeness is an essential part of the lattice convention. The zero-bracket <module> $\mathbb F_p$ satisfies the bracket inclusion but has torsion, and its additive <group> is not uniform. Thus allowing arbitrary torsion modules would make the categorical assertion false.

The basic structural facts behind the construction can be seen from the power layers. Write $P_n=G^{p^n}$ with $P_0=G$. Collection for a <powerful pro-p group> gives
$$
[P_r,P_s]\subseteq P_{r+s+\epsilon},\qquad P_n=\{g^{p^n}:g\in G\}.
$$
For odd $p$, the power lifting is exactly the successive-correction argument of Question 3, followed by compactness; at $p=2$ the stronger fourth-power commutator condition makes the corresponding collection corrections work. The maps between successive layers are surjective linear maps. Uniformity makes their finite dimensions equal, so these maps are isomorphisms. Comparing the first layer in which two elements differ now shows that the power map $P_n\to P_{n+1}$ is injective, while the power-set formula makes it surjective. Thus all the roots used below exist uniquely in the indicated layer. If $g_1,\ldots,g_d$ lift a basis of $G/P_1$, the images of $g_i^{p^n}$ form a basis of $P_n/P_{n+1}$. Successively choosing their coefficients modulo $p$ gives the unique ordered expression
$$
g=g_1^{\lambda_1}\cdots g_d^{\lambda_d},\qquad \lambda_i\in\mathbb Z_p.
$$
Existence follows by lifting one layer at a time and taking a limit; uniqueness follows by comparing the first nonzero coefficient layer. In particular $[G:P_n]=p^{nd}$ and these layers form a neighbourhood basis. These are the power-layer and coordinate facts needed in the proof, rather than an assumption that an arbitrary <pro-p group> has unique roots.

On the underlying set of $G$, set the additive zero to $1$, the additive negative of $x$ to $x^{-1}$, and define
$$
\lambda\cdot_Lx=x^\lambda,\qquad
x+_Ly=\lim_{n\to\infty}(x^{p^n}y^{p^n})^{p^{-n}},\qquad
[x,y]_L=\lim_{n\to\infty}[x^{p^n},y^{p^n}]^{p^{-2n}}.
$$
The <p-adic integers> act through limits of integer powers in the closed <cyclic subgroup> generated by $x$. In the second formula the product belongs to $P_n$; in the third the <group commutator> belongs to $P_{2n+\epsilon}$. The symbols $p^{-n}$ and $p^{-2n}$ denote the unique group roots, not unrestricted division in a <group>. We next justify convergence and the <Lie algebra> laws together.

A useful concrete tool is a complete normed <group algebra> containing $G$. In its <completed group algebra>, put $b_i=g_i-1$. Ordered-coordinate uniqueness gives unique expansions $\sum_{\alpha\in\mathbb N^d}c_\alpha b_1^{\alpha_1}\cdots b_d^{\alpha_d}$ with $c_\alpha\in\mathbb Z_p$. To see why, first work modulo $p$ and $P_n$: the ordered products of the $g_i$ with exponents below $p^n$ form the regular basis, and the change to the corresponding products of $g_i-1$ is triangular with diagonal entries one. Take inverse limits and then lift the coefficient digits successively in powers of $p$. Define the weight
$$
v\left(\sum_\alpha c_\alpha b^\alpha\right)=\inf_\alpha\{v_p(c_\alpha)+\epsilon|\alpha|\}.
$$
It is a genuine separated, submultiplicative weight. Indeed reordering $b_jb_i$ produces a group-commutator correction in $P_\epsilon$; the binomial expansion of a $p^\epsilon$th power gives that correction weight at least $2\epsilon$, so collection never decreases total weight. Also $v(pc)=1+v(c)$. Inverting $p$ and completing therefore gives a <Banach algebra> $B$ over $\mathbb Q_p$. For $g\in G$, ordered coordinates show
$$
v(g-1)=\epsilon+\max\{n:g\in P_n\},
$$
with value infinity at $g=1$. Thus the induced <topology> on $G$ is exactly its original <topology>. This construction supplies the ambient algebra without presupposing the <uniform pro-p group and powerful Lie lattice correspondence>. The weighted construction, including the case $p=2$, is described in https://smf.emath.fr/system/files/filepdf/smf_ast_423.pdf[Equivariant D-modules on rigid analytic spaces, Section 6.5].

Since $\epsilon>1/(p-1)$, the <p-adic logarithm> and <p-adic exponential> converge on the relevant balls in $B$:
$$
\log(1+b)=\sum_{k\geq1}\frac{(-1)^{k+1}b^k}{k},\qquad
\exp(a)=\sum_{k\geq0}\frac{a^k}{k!}.
$$
The estimates $v_p(k!)\leq k/(p-1)$ and $v_p(k)\leq\log_p k$ show that term weights tend to infinity. Formal substitution is legitimate there and proves that the two maps are inverse. They preserve the leading weight. In particular $\log$ embeds the compact set $G$ homeomorphically into $B$, and $\log(g^{p^n})=p^n\log g$.

Put $a=\log x$ and $b=\log y$. Expanding the convergent <Baker--Campbell--Hausdorff formula> in $B$ gives
$$
p^{-n}\log(x^{p^n}y^{p^n})\longrightarrow a+b,\qquad
p^{-2n}\log([x^{p^n},y^{p^n}])\longrightarrow ab-ba.
$$
The first expansion has linear part $p^n(a+b)$ and all other terms have degree at least two in $p^na,p^nb$. The second has leading term $p^{2n}(ab-ba)$ and all remaining terms have degree at least three. After division by the displayed powers of $p$, the extra factor of $p^n$ forces those errors to zero. The normalized expressions are logarithms of the unique roots already specified. Since $\log G$ is compact and closed in $B$, both limits belong to $\log G$. Scalar multiplication also remains in $\log G$ by continuity of powers. Consequently $\log G$ is a <module> over $\mathbb Z_p$, closed under the associative-algebra <Lie bracket> $ab-ba$. Bilinearity, alternation and the <Jacobi identity> follow by expanding products in the <associative algebra> $B$. Transporting these operations back gives exactly $L_G$ above.

The commutator-layer inclusion places every normalized bracket root in $P_\epsilon$. Since $\log P_\epsilon=p^\epsilon\log G$ and this set is compact, passage to the limit proves $[L_G,L_G]\subseteq p^\epsilon L_G$. Addition modulo $pL_G$ is the original multiplication modulo $P_1$: collection shows $(x^{p^n}y^{p^n})^{p^{-n}}\equiv xy\pmod {P_1}$, as the nonlinear errors lie at least one layer deeper. Thus $L_G/pL_G$ has dimension $d$, with basis $e_i=\log g_i$. Given $a\in\log G$, write its residue as $\sum_i\lambda_{0i}e_i$ and repeat on $(a-\sum_i\lambda_{0i}e_i)/p$. This iterative digit lifting converges because the remainders stay in the bounded compact set $\log G$. It gives $a=\sum_i\lambda_i e_i$ with $\lambda_i\in\mathbb Z_p$. A nontrivial relation among the $e_i$ could be divided by the smallest power of $p$ among its coefficients, contradicting their independence modulo $p$. Hence $L_G$ is free of rank $d$, proving that it is a <powerful Lie lattice>.

Conversely, let $L$ be a <powerful Lie lattice>. In $L\otimes_{\mathbb Z_p}\mathbb Q_p$, define
$$
x*y=\operatorname{BCH}(x,y)
=x+y+\frac12[x,y]+\frac1{12}\bigl([x,[x,y]]+[y,[y,x]]\bigr)+\cdots.
$$
The formal <Baker--Campbell--Hausdorff formula> and its coefficient estimate are the algebraic ingredients used here. More precisely, the degree-$m$ component can be expressed as an integral Lie polynomial divided by a number of $p$-adic valuation at most $\lfloor(m-1)/(p-1)\rfloor$. One way to obtain this estimate is to bound the associative coefficients of $\log(\exp X\exp Y)$ and use an integral ordered basis of the free <Lie algebra>. The denominator bound $v_p(m!)+\lfloor\log_p s_p(m)\rfloor$, where $s_p(m)$ is the base-$p$ digit sum, is at most $\lfloor(m-1)/(p-1)\rfloor$. A precise primary reference for that denominator estimate is https://arxiv.org/abs/2012.03818[Smallest common denominators for the homogeneous components of the Baker-Campbell-Hausdorff series]. A length-$m$ <Lie bracket> in $L$ lies in $p^{\epsilon(m-1)}L$. Thus the degree-$m$ term belongs to
$$
p^{\epsilon(m-1)-\lfloor(m-1)/(p-1)\rfloor}L.
$$
These exponents are nonnegative and tend to infinity; for $m\geq2$ they are at least one. This proves integral convergence, continuity and $x*y\equiv x+y\pmod {pL}$. Associativity follows from the formal identity $\exp(\operatorname{BCH}(X,Y))=\exp X\exp Y$ in the completed <universal enveloping algebra>. Substitution of three elements is justified by the same valuation estimates, so the two associative expressions agree. The identity is $0$, the inverse is $-x$, and $x^{*k}=kx$ because every nonlinear term involving only $x$ vanishes.

For powerfulness, formal conjugation gives
$$
\exp(-x)\exp(-y)\exp(x)=\exp(-e^{-\operatorname{ad}x}y).
$$
The difference $\delta=y-e^{-\operatorname{ad}x}y$ lies in $p^\epsilon L$: its $k$th term has valuation at least $k\epsilon-v_p(k!)\geq\epsilon$ for $k\geq1$. The group <commutator> is therefore $(-y+\delta)*y$. Its linear term is $\delta$. Every nonlinear Lie term contains $\delta$, since it vanishes when $\delta=0$, and the extra divisibility makes all those terms lie in $p^\epsilon L$ too. Hence $[(L,*),(L,*)]\subseteq p^\epsilon L$. The ideals $p^nL$ are open normal <subgroups> for $*$, and their finite quotients have order $p^{nd}$. The <group> is consequently a <pro-p group>. Its power sets are exactly $p^nL$, its lower-series indices are constantly $p^d$, and a basis of $L$ topologically generates it by the same successive digit lifting. \b[The BCH group $(L,*)$ is uniform.]

To check the inverse constructions, powers in the <Baker--Campbell--Hausdorff formula> group are ordinary multiples in $L$. Therefore
$$
p^{-n}\operatorname{BCH}(p^nx,p^ny)\longrightarrow x+y,
$$
and the similarly normalized <group commutator> tends to $[x,y]$. The limit constructions recover the original <Lie algebra> exactly. In the other direction, the ambient <Banach algebra> construction gives $\log(xy)=\operatorname{BCH}(\log x,\log y)$, so the recovered operation is the original multiplication of $G$.

Finally a continuous <group homomorphism> between <uniform pro-p groups> preserves integer powers and powers with exponents in the <p-adic integers>, preserves the unique roots in the power layers, and commutes with their limits. It therefore becomes a linear <Lie algebra homomorphism>. Conversely a linear <Lie algebra homomorphism> between finite free <modules> is continuous and preserves every term of the convergent <Baker--Campbell--Hausdorff formula>, hence is a continuous <group homomorphism> for $*$. The constructions preserve identity maps and composition, and the inverse identifications are natural. \b[They are mutually inverse functors, giving the stated category correspondence with the finite-free lattice convention.]