Surjectivity of good reduction over a local field (source code)

= Surjectivity of good reduction over a local field

If an <elliptic curve> has <good reduction> over a <local field> $K$, its integral projective model is smooth. Every point over the <residue field> lifts by the <Hensel lemma>, applied in a chart with a unit <partial derivative>. Thus reduction gives an exact sequence $0\to E_1(K)\to E(K)\to\widetilde E(k)\to0$. The <kernel of reduction of an elliptic curve> is the <maximal ideal> of the <valuation ring>, with the <formal group of an elliptic curve> as its <group operation>.