Root correction criterion for uniformity (source code)

= Root correction criterion for uniformity
{title2=$u\mapsto u^p:U_j/U_{j+1}\longrightarrow U_{j+1}/U_{j+2}$}

For odd $p$ and a finitely generated <powerful pro-p group>, put $U_j=G^{p^j}$. The displayed <group homomorphisms> are surjective. If one has a nonzero <kernel>, choose $x\in U_j\setminus U_{j+1}$ with $x^p\in U_{j+2}$. Successive corrections $x\mapsto xu_r$, with $u_r\in U_r$, cancel its $p$-th power one layer at a time, using $(xu_r)^p\equiv x^pu_r^p\pmod {U_{r+2}}$. <Compactness> and the separated power filtration give a nonidentity limit of order $p$. Thus a <torsion-free group> has constant layer indices and is a <uniform pro-p group>. Conversely constant indices make every displayed map injective; comparison at the first differing power layer proves that $x\mapsto x^p$ is injective, so there is no nontrivial torsion.