Solution (source code)

= Solution

An <elliptic curve> has <good reduction> over $K$ if it admits an integral <Weierstrass equation of an elliptic curve> with unit <elliptic-curve discriminant>. Equivalently, the reduction of its <Minimal Weierstrass equation> is a nonsingular cubic over the <residue field> $k$. Its smooth integral projective model is a <group scheme> with the point $O$ as identity.

Choose <homogeneous coordinates> in the <valuation ring> $\mathcal O_K$ with at least one coordinate a unit, and reduce them modulo its <maximal ideal> $\mathfrak m_K$. This defines $\operatorname{red}:E(K)\to\widetilde E(k)$. The <chord-and-tangent group law> extends over the smooth integral model, so reduction is a <group homomorphism>. For any point of $\widetilde E(k)$, choose an affine projective chart containing it. Smoothness means some <partial derivative> of its equation is nonzero in $k$. Lift the other coordinate arbitrarily and apply the <Hensel lemma> to the coordinate with unit derivative. This constructs a point of $E(K)$ above the prescribed point, proving the <surjectivity of good reduction over a local field>.

The <kernel of reduction of an elliptic curve> consists precisely of points reducing to $O$. The parameter $t=-x/y$ at $O$ gives a bijection between this kernel and $\mathfrak m_K$: the integral formal-coordinate series solve the equation uniquely near $O$. Addition in these coordinates is the <formal group of an elliptic curve>, not ordinary addition in $\mathfrak m_K$. Thus
$$
\boxed{0\longrightarrow E_1(K)\longrightarrow E(K)\xrightarrow{\operatorname{red}}\widetilde E(k)\longrightarrow0,\qquad E_1(K)\simeq\widehat E(\mathfrak m_K).}
$$
Here the <group operation> on the last expression is its <formal group law>.