Solution (source code)

= Solution

<Kummer theory> begins with the exact sequence
$$
1\longrightarrow\mu_n\longrightarrow\overline K^\times
\xrightarrow{(cdot)^n}\overline K^\times\longrightarrow1.
$$
<Galois cohomology> and Hilbert theorem 90 identify
$$
H^1(K,\mu_n)\cong K^\times/K^{\times n},
$$
so cyclic extensions of exponent dividing $n$ are described by adjoining $n$th roots when $K$ contains $\mu_n$.

For an <elliptic curve> $E/K$, multiplication by $n$ gives the <Kummer exact sequence of an elliptic curve>
$$
0\longrightarrow E[n]\longrightarrow E(\overline K)
\xrightarrow{[n]}E(\overline K)\longrightarrow0.
$$
Its connecting homomorphism is the injective <Kummer map of an elliptic curve>
$$
E(K)/nE(K)\hookrightarrow H^1(K,E[n]),
\qquad
P\longmapsto(\sigma\mapsto\sigma Q-Q),
$$
where $nQ=P$. Passing to the finite <division field of an elliptic curve> $K(E[n])$ makes $E[n]$ constant. Rational functions whose divisors are $n(T)-n(O)$ then express the classes through finitely many elements of $K(E[n])^\times/K(E[n])^{\times n}$.

Let $S$ contain the primes above $n$, the primes of <bad reduction of an elliptic curve> and the finitely many primes introduced by these functions. The local theory of good reduction shows that every Kummer class coming from $E(K)$ is unramified outside $S$, so it lies in an <S-unramified power class group>. Such a group is finite: valuations outside $S$ vanish modulo $n$, the <ideal class group> is finite, and the <Dirichlet unit theorem> makes the group of $S$-units modulo $n$th powers finite. The kernel created by passing to $K(E[n])$ is finite by finite-group <Galois cohomology>. Hence
$$
\boxed{E(K)/nE(K)\text{ is finite}.}
$$
This is the <Kummer-theoretic proof of the weak Mordell-Weil theorem>. Combining it with the <height descent lemma> proves the <Mordell-Weil theorem>: $E(K)$ is a finitely generated abelian group.