Prime-to-p torsion lifts uniquely at good reduction (source code)

= Prime-to-p torsion lifts uniquely at good reduction
{title2=$E(K)[q^\infty]\cong\widetilde E(k)[q^\infty],\quad q\ne p$}

For <good reduction of an elliptic curve> over a complete <local field> of residue characteristic $p$, smoothness and the <Hensel lemma> make reduction surjective. Its kernel is a <formal group> on the maximal ideal, where multiplication by $q^m$, $q\ne p$, is bijective by <prime-to-residue-characteristic multiplication on a formal group>. Thus there is no nonzero $q$-power torsion in the kernel. Given a lift $P$ of a reduced point killed by $q^m$, choose the unique kernel point $R$ with $q^mR=q^mP$. Then $P-R$ is a torsion lift. This proves both surjectivity and uniqueness of torsion lifting. For finite residue field these groups are finite.