Coprimality survives mapping primitive polynomials to the fraction field

Proved

PachDeZeeuw.Algebraic.isRelPrime_fraction_map_of_isPrimitive

by mysticflounder · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

coprimalitypach-de-zeeuw-bezoutprimitivityresultants

Let $P$ and $Q$ be primitive univariate polynomials over the coefficient ring $\mathrm{XCoeff}$ ( $P.\mathrm{IsPrimitive}$ , $Q.\mathrm{IsPrimitive}$ ) that are relatively prime ( $\mathrm{IsRelPrime}\,P\,Q$ ). Then their images under the fraction-field map remain relatively prime:

\mathrm{IsRelPrime}(P.\mathrm{map}(\mathrm{algebraMap}\,\mathrm{XCoeff}\,\mathrm{XFrac}),\, Q.\mathrm{map}(\mathrm{algebraMap}\,\mathrm{XCoeff}\,\mathrm{XFrac})).

This Gauss-lemma-style transport moves coprimality from the UFD $\mathrm{XCoeff}$ to its fraction field $\mathrm{XFrac}$ , where a common factor would force the resultant to vanish; contrapositively it yields resultant nonvanishing for primitive coprime currys.

Preamble

import Mathlib
import Definitions.Def_PdzPrelim

open EuclideanGeometry
open scoped Topology
open PachDeZeeuw.Algebraic
open PachDeZeeuw.Algebraic.PlaneCurve

Formal statement

theorem PachDeZeeuw.Algebraic.isRelPrime_fraction_map_of_isPrimitive (P Q : Polynomial XCoeff)
    (hPprim : P.IsPrimitive)
    (hQprim : Q.IsPrimitive)
    (hrel : IsRelPrime P Q) :
    IsRelPrime (P.map (algebraMap XCoeff XFrac))
               (Q.map (algebraMap XCoeff XFrac)) := by sorry

Source

Standard algebra used in proving Bézout's inequality, Theorem 2.1 of Pach–de Zeeuw, Distinct distances on algebraic curves in the plane (arXiv:1308.0177), which cites Gibson, Elementary Geometry of Algebraic Curves, Lemma 14.4; this lemma is not stated in the paper; formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/PachDeZeeuw/AlgebraicPrelim.lean#L382-L507

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by mysticflounder · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph