Unique common root of a split separable polynomial is rational #
Theorem statement: Polynomial.mem_range_of_unique_common_root
(059deab2-7e60-5275-95da-b2b308cb1ae6), by Claude, 2026-09-05.
Proof: submission 1be1f735-9591-5b4c-87da-71c8bc6713bf, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $F$ and $L$ be fields with $L$ an $F$-algebra, and let $A, B \in F[X]$. Assume $A \neq 0$, that
the image $A^{L}$ of $A$ under the coefficient map $F \to L$ splits over $L$ (Polynomial.Splits
for a polynomial over a field, i.e. $A^{L}$ factors into linear factors in $L[X]$), and that the
multiset of roots of $A^{L}$ has no repetitions, so that $A^{L}$ has only simple roots. Let $x \in L$ satisfy $A(x) = 0$ and $B(x) = 0$, where the evaluation is via the structure map $F \to L$, and
suppose $x$ is the only common zero: every $y \in L$ with $A(y) = 0$ and $B(y) = 0$ equals $x$. Then
$x$ lies in the range of algebraMap F L, i.e. $x$ is the image of an element of $F$. Note that $B$
is not assumed nonzero and no separability or normality hypothesis is imposed on the extension $L/F$
beyond the splitting and simplicity of the roots of $A$.
This is a descent criterion for a point of $L$ to be $F$-rational, obtained by looking at the
greatest common divisor of $A$ and $B$ in $F[X]$, whose reduction over $L$ must be linear. It is
used in the treatment of modular curves, for instance by
ModularCurve.full_eq_adjoin_primes and
ModularCurve.full_sq_eq_adjoin, to show that certain
coordinates cut out by a pair of polynomial relations already lie in the base field.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_Polynomial_mem_range_of_unique_common_root.lean
<!-- Generated by add_prove2me_provenance.py -->