Documentation

MazurTorsion.NumberTheory.XOneEighteenDescent

Quotient and arithmetic descent identities for X₁(18) #

The order-three automorphism of the order-eighteen sextic has invariant functions

u = (x³ - 3x + 1)/(x(x-1)), v = y/(x(x-1)),

which satisfy

v² = u² - 4u + 12.

This file parameterizes that rational conic, identifies the degree-three fiber as the cyclic cubic

z³ - uz² + (u-3)z + 1,

and records its orbit factorization and square discriminant. After the conic parameter is introduced, the cleared cubic has discriminant

(t²+3)²(7t²+6t+3)².

The two quadratic factors are explicit norms in Eisenstein coordinates. Writing ω²+ω+1=0, the second is

N((3+ω)m + (1-ω)n) = 7m²+6mn+3n²,

and N(3+ω)=7. We prove these norm identities, multiplicativity, two primitive-form Bézout identities, and the fact that the two norm forms cannot both be divisible by 7 for coprime integer parameters.

These are algebraic and local prerequisites for the classical π = 3+ω descent. They do not construct the induced endomorphism of the Jacobian, prove π-surjectivity on its Mordell--Weil group, determine its torsion, or classify rational points.

The rational conic quotient #

The conic abscissa obtained from a line through (u,v)=(1,3).

Equations
Instances For

    The conic ordinate obtained from the same line.

    Equations
    Instances For

      The displayed parametrization lies on the invariant conic.

      The slope used to recover the conic parameter away from u=1.

      Equations
      Instances For
        theorem MazurTorsion.XOneEighteenDescent.conic_parameter_inverse (u v : ) (hu : u 1) (hconic : v ^ 2 = u ^ 2 - 4 * u + 12) :
        have t := conicSlope u v; t ^ 2 1 conicU t = u conicV t = v

        Away from the base point's vertical fiber, the slope construction recovers both conic coordinates.

        theorem MazurTorsion.XOneEighteenDescent.conic_at_one_iff (v : ) :
        v ^ 2 = 1 ^ 2 - 4 * 1 + 12 v = 3 v = -3

        The exceptional affine conic fiber u=1 consists of v=±3.

        theorem MazurTorsion.XOneEighteenDescent.conic_rational_parameterization (u v : ) (hconic : v ^ 2 = u ^ 2 - 4 * u + 12) :
        u = 1 (v = 3 v = -3) ∃ (t : ), t ^ 2 1 conicU t = u conicV t = v

        Every rational affine point on the invariant conic is either one of the two exceptional points over u=1, or comes from the displayed one-parameter family.

        The cyclic cubic fiber #

        The degree-three fiber above a quotient abscissa u.

        Equations
        Instances For

          The exceptional quotient fiber u=1 has no rational abscissa.

          The invariant abscissa of a noncuspidal point satisfies its cubic fiber equation.

          A noncuspidal rational abscissa never lies over the exceptional quotient value u=1.

          Product over the three-element Möbius orbit, viewed as a degree-three norm polynomial.

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

            The orbit norm is exactly the cyclic cubic fiber polynomial.

            The standard discriminant formula for a cubic a z³ + b z² + c z + d.

            Equations
            Instances For

              The cyclic cubic fiber has square discriminant.

              The conic-parameterized cubic with its sole denominator cleared.

              Equations
              Instances For

                Clearing the conic denominator gives clearedFiber.

                theorem MazurTorsion.XOneEighteenDescent.clearedFiber_eq_zero (t z : ) (ht : t ^ 2 1) (hroot : fiberCubic (conicU t) z = 0) :

                A root of the parameterized fiber gives a root of the cleared cubic.

                The homogeneous cubic obtained by writing the conic parameter as t=m/n.

                Equations
                Instances For

                  Substitution t=m/n turns the cleared cubic into its homogeneous form after multiplication by .

                  A root of the cleared rational-parameter cubic is a root of the primitive homogeneous cubic attached to its canonical fraction.

                  theorem MazurTorsion.XOneEighteenDescent.homogeneousFiber_discriminant (m n : ) :
                  cubicDiscriminant (m ^ 2 - n ^ 2) (-(m ^ 2 - 6 * m * n - 3 * n ^ 2)) (-2 * m ^ 2 - 6 * m * n) (m ^ 2 - n ^ 2) = (m ^ 2 + 3 * n ^ 2) ^ 2 * (7 * m ^ 2 + 6 * m * n + 3 * n ^ 2) ^ 2

                  The homogeneous cubic discriminant is the product of the squares of the two quadratic norm forms.

                  Every rational noncuspidal point on the sextic admits the explicit conic parameter and is a root of the resulting denominator-free cubic.

                  Canonical numerator-denominator coordinates sharpen the preceding statement to primitive integer parameters.

                  theorem MazurTorsion.XOneEighteenDescent.clearedFiber_discriminant (t : ) :
                  cubicDiscriminant (t ^ 2 - 1) (-(t ^ 2 - 6 * t - 3)) (-2 * t ^ 2 - 6 * t) (t ^ 2 - 1) = (t ^ 2 + 3) ^ 2 * (7 * t ^ 2 + 6 * t + 3) ^ 2

                  The coefficient discriminant of the cleared cubic factors into two squared quadratic forms.

                  theorem MazurTorsion.XOneEighteenDescent.fiber_discriminant_parameter_factorization (t : ) (ht : t ^ 2 1) :
                  conicU t ^ 2 - 3 * conicU t + 9 = (t ^ 2 + 3) * (7 * t ^ 2 + 6 * t + 3) / (t ^ 2 - 1) ^ 2

                  The square root of the fiber discriminant before clearing denominators factors as displayed.

                  Eisenstein-coordinate norm identities #

                  Multiplication in coordinates a+bω, where ω²+ω+1=0.

                  Equations
                  Instances For

                    The norm of the Eisenstein coordinate pair a+bω.

                    Equations
                    Instances For

                      Complex conjugation in coordinates a+bω, using conj(ω)=ω²=-1-ω.

                      Equations
                      Instances For

                        Multiplication by the conjugate gives the rational integer norm.

                        The Eisenstein prime above 7, represented by π=3+ω.

                        Equations
                        Instances For

                          The coordinate factorization of the rational prime 7 as π·conj(π).

                          The index-seven lattice cut out by multiplication by π has the single congruence 2a+b ≡ 0 mod 7.

                          A factor of π forces a factor of 7 in the norm.

                          The first quadratic factor is an Eisenstein norm after clearing a rational parameter t=m/n.

                          The second quadratic factor is the norm of πm + (1-ω)n.

                          Coordinate identity behind (3+ω)m + (1-ω)n = (3m+n) + (m-n)ω.

                          The second norm argument is divisible by π exactly when the denominator parameter is divisible by 7.

                          The two primitive quadratic norm forms.

                          Equations
                          Instances For

                            The norm form associated to the Eisenstein prime above seven.

                            Equations
                            Instances For
                              theorem MazurTorsion.XOneEighteenDescent.homogeneousFiber_discriminant_integer (m n : ) :
                              cubicDiscriminant (m ^ 2 - n ^ 2) (-(m ^ 2 - 6 * m * n - 3 * n ^ 2)) (-2 * m ^ 2 - 6 * m * n) (m ^ 2 - n ^ 2) = (firstParameterForm m n) ^ 2 * (piParameterForm m n) ^ 2

                              For integer homogeneous parameters, the two factors in the cubic discriminant are exactly the two named norm forms.

                              A Bézout-style identity eliminating the denominator parameter.

                              A complementary Bézout-style identity eliminating the numerator parameter.

                              For primitive integer parameters, the two Eisenstein norm forms cannot both be divisible by the rational prime below π.

                              The complete elementary descent package obtained here from a noncuspidal rational point: primitive homogeneous parameters, the homogeneous cubic equation, and the local exclusion of a simultaneous factor of 7 in its two Eisenstein norm factors.