Solution (source code)

= Solution

An <isogeny of elliptic curves> over $k$ is a nonconstant $k$-morphism $\varphi:E_1\to E_2$ which sends $O_1$ to $O_2$. A nonconstant morphism of smooth projective curves is finite and surjective. Its compatibility with the <elliptic curve group law from Riemann-Roch> can be seen without assuming it in the definition.

Identify a point $P$ with the degree-zero <divisor class> $[P-O_1]$. A <finite morphism> pushes forward divisors, and pushes a <principal divisor> to the <principal divisor> of the norm of its rational function. It therefore induces a <group homomorphism> on <degree-zero Picard groups of a curve>. On geometric points, the pushforward of $[P-O_1]$ is $[\varphi(P)-O_2]$. Since point addition is addition of these <divisor classes>, this proves
$$
\boxed{\varphi(P+Q)=\varphi(P)+\varphi(Q).}
$$
The equality is defined over $k$, so in particular it holds on the <groups> of $k$-rational points and after every <field> extension. The argument also covers inseparable <isogenies of elliptic curves>; separability is not part of the definition.