Subgroup generator bound for a powerful finite p-group (source code)

= Subgroup generator bound for a powerful finite p-group
{title2=$d(H)\le d(G)$}

For odd $p$, a <subgroup> $H$ of a finite <powerful p-group> $G$ satisfies $d(H)\le d(G)$. Here $d$ is the <dimension> of the <Frattini quotient>. Set $K=H\cap G^p$, $V=G/G^p$, $W=G^p/G^{p^2}$, and $A=HG^p/G^p$. The onto power map $\theta:V\to W$ sends $A$ into the image of $H^p$ in $K/\Phi(K)$. Since $\Phi(K)\le G^{p^2}$, this image has <dimension> at least $\dim\theta(A)$. Also $\Phi(K)\le\Phi(H)\le K$. Induction on $|G|$, applied to the powerful <subgroup> $G^p$, gives $d(K)\le\dim W$. Consequently
$$
d(H)\le\dim A+\dim W-\dim\theta(A)\le\dim W+\dim\ker\theta=\dim V=d(G).
$$
The last inequality is <rank-nullity theorem>.