The dual-kernel cubic for the order-seven isogeny

The cubic below is characterized in OrderSevenDualKernelPullback: after substitution of the explicit Vélu abscissa and clearing its kernel denominator, it becomes the source seventh division polynomial. This is the pullback identity for the kernel of the dual isogeny. The present file records the cubic and proves that it has no rational root on a nonsingular member of the source family.

The proof makes the fixed real-cyclotomic cubic z³ + z² - 2z - 1 appear by an explicit rational change of primitive element. That cubic has no rational root by the rational-root theorem.

def MazurTorsion.Kubert.orderSevenDualKernelPolynomial (d x : ℚ) : ℚ

The cubic whose geometric roots are the three nonzero abscissae of the dual kernel of the explicit order-seven isogeny.

Equations

• One or more equations did not get rendered due to their size.

theorem MazurTorsion.Kubert.orderSevenDualKernelPolynomial_ne_zero (d x : ℚ) [(orderSevenFamily d).IsElliptic] : orderSevenDualKernelPolynomial d x ≠ 0

On a nonsingular order-seven Tate curve, the dual-kernel cubic has no rational root.