Documentation

MazurTorsion.NumberTheory.XOneThirteenFiniteField

Finite-field certificates for the `X₁(13)` sextic #

This file records elementary certificates for the reductions modulo 3 and 5 of

y² = x⁶ + 2x⁵ + x⁴ + 2x³ + 6x² + 4x + 1.

Both reduced sextics are separable: explicit Bézout coefficients for them and their derivatives are checked in the kernel. The affine solutions over ZMod 3 are exactly

(0, 1), (0, -1), (-1, 1), (-1, -1).

For the usual weighted-projective compactification of a monic even-degree hyperelliptic equation, the normalized infinity chart has equation η² = 1. We define and enumerate those normalized directions, obtaining two of them. The resulting sum type is only an explicit finite-field point certificate; this file does not assert an equivalence with a projective-curve API. We also enumerate the same equation in transparent quadratic-algebra presentations of 𝔽₉ and 𝔽₂₅. The nonsquare and inverse certificates for those presentations are checked by decide, as are the point counts.

In particular, none of these calculations proves a classification over ℚ, a theorem about the Jacobian, or injectivity of reduction on rational points.

@[reducible, inline]

abbrev MazurTorsion.XOneThirteenFiniteField.F3 :

The three-element residue field used for the order-thirteen point count.

Equations

MazurTorsion.XOneThirteenFiniteField.F3 = ZMod 3

Instances For

noncomputable def MazurTorsion.XOneThirteenFiniteField.sextic :

The order-thirteen hyperelliptic sextic reduced modulo 3.

Equations

MazurTorsion.XOneThirteenFiniteField.sextic = Polynomial.X ^ 6 + 2 * Polynomial.X ^ 5 + Polynomial.X ^ 4 + 2 * Polynomial.X ^ 3 + 6 * Polynomial.X ^ 2 + 4 * Polynomial.X + 1

Instances For

def MazurTorsion.XOneThirteenFiniteField.sexticValue (x : F3) :

A computable presentation of the sextic's value function.

Equations

MazurTorsion.XOneThirteenFiniteField.sexticValue x = x ^ 6 + 2 * x ^ 5 + x ^ 4 + 2 * x ^ 3 + 6 * x ^ 2 + 4 * x + 1

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.eval_sextic (x : F3) :

Polynomial.eval x sextic = sexticValue x

Evaluation of the reduced sextic agrees with the displayed formula.

theorem MazurTorsion.XOneThirteenFiniteField.derivative_sextic :

Polynomial.derivative sextic = Polynomial.X ^ 4 + Polynomial.X ^ 3 + 1

The formal derivative of the reduced sextic.

noncomputable def MazurTorsion.XOneThirteenFiniteField.bezoutLeft :

Left Bézout coefficient for the sextic and its derivative.

Equations

MazurTorsion.XOneThirteenFiniteField.bezoutLeft = Polynomial.X ^ 3 + 1

Instances For

noncomputable def MazurTorsion.XOneThirteenFiniteField.bezoutRight :

Right Bézout coefficient for the sextic and its derivative.

Equations

MazurTorsion.XOneThirteenFiniteField.bezoutRight = -(Polynomial.X ^ 5 + Polynomial.X ^ 4 + Polynomial.X)

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.sextic_derivative_bezout :

bezoutLeft * sextic + bezoutRight * Polynomial.derivative sextic = 1

Explicit gcd certificate for the sextic and its derivative.

theorem MazurTorsion.XOneThirteenFiniteField.sextic_isCoprime_derivative :

IsCoprime sextic (Polynomial.derivative sextic)

The reduced sextic is coprime to its derivative.

theorem MazurTorsion.XOneThirteenFiniteField.sextic_separable :

sextic.Separable

The reduction modulo 3 is separable.

theorem MazurTorsion.XOneThirteenFiniteField.sextic_squarefree :

Squarefree sextic

In particular, the reduced sextic is squarefree.

theorem MazurTorsion.XOneThirteenFiniteField.sextic_or_derivative_ne_zero (x : F3) :

Polynomial.eval x sextic ≠ 0 ∨ Polynomial.eval x (Polynomial.derivative sextic) ≠ 0

The sextic and its derivative have no common root over F3.

def MazurTorsion.XOneThirteenFiniteField.AffineSolution :

An affine solution of the reduced hyperelliptic equation.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeAffineSolution :

Fintype AffineSolution

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeAffineSolution = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.affine_solution_iff (x y : F3) :

y ^ 2 = sexticValue x ↔ x = 0 ∧ (y = 1 ∨ y = -1) ∨ x = -1 ∧ (y = 1 ∨ y = -1)

Complete enumeration of affine solutions over F3.

theorem MazurTorsion.XOneThirteenFiniteField.affine_solution_polynomial_iff (x y : F3) :

y ^ 2 = Polynomial.eval x sextic ↔ x = 0 ∧ (y = 1 ∨ y = -1) ∨ x = -1 ∧ (y = 1 ∨ y = -1)

Polynomial-evaluation form of the complete affine enumeration.

theorem MazurTorsion.XOneThirteenFiniteField.card_affineSolution :

Fintype.card AffineSolution = 4

There are exactly four affine solutions over F3.

def MazurTorsion.XOneThirteenFiniteField.IsAffineCuspX (x : F3) :

The two affine abscissas occurring modulo 3. They are precisely the reductions of the rational affine cusp abscissas from the sextic model.

Equations

MazurTorsion.XOneThirteenFiniteField.IsAffineCuspX x = (x = 0 ∨ x = -1)

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instDecidableIsAffineCuspX (x : F3) :

Decidable (IsAffineCuspX x)

Equations

MazurTorsion.XOneThirteenFiniteField.instDecidableIsAffineCuspX x = MazurTorsion.XOneThirteenFiniteField.instDecidableIsAffineCuspX._aux_1 x

theorem MazurTorsion.XOneThirteenFiniteField.affine_solution_is_cusp_value (x y : F3) :

y ^ 2 = sexticValue x → IsAffineCuspX x

Computable form of affine_solution_is_cusp.

theorem MazurTorsion.XOneThirteenFiniteField.affine_solution_is_cusp (x y : F3) :

y ^ 2 = Polynomial.eval x sextic → IsAffineCuspX x

Every affine F3-solution has a cusp abscissa.

theorem MazurTorsion.XOneThirteenFiniteField.cusp_abscissa_solution_iff (x : F3) :

IsAffineCuspX x → ∀ (y : F3), y ^ 2 = sexticValue x ↔ y = 1 ∨ y = -1

The affine equation has two ordinates over each cusp abscissa.

theorem MazurTorsion.XOneThirteenFiniteField.eval_derivative_sextic (x : F3) :

Polynomial.eval x (Polynomial.derivative sextic) = x ^ 4 + x ^ 3 + 1

The derivative has the following computable value function.

theorem MazurTorsion.XOneThirteenFiniteField.affine_jacobian_nonsingular (x y : F3) :

y ^ 2 = sexticValue x → x ^ 4 + x ^ 3 + 1 ≠ 0 ∨ 2 * y ≠ 0

Explicit affine Jacobian certificate: at a solution, the two partial derivatives -f'(x) and 2y cannot both vanish.

theorem MazurTorsion.XOneThirteenFiniteField.affine_jacobian_nonsingular_polynomial (x y : F3) (hxy : y ^ 2 = Polynomial.eval x sextic) :

Polynomial.eval x (Polynomial.derivative sextic) ≠ 0 ∨ 2 * y ≠ 0

Polynomial-evaluation form of the affine Jacobian certificate.

theorem MazurTorsion.XOneThirteenFiniteField.sextic_monic :

The reduced sextic is monic.

def MazurTorsion.XOneThirteenFiniteField.InfinityDirection :

A normalized direction in the infinity chart of the monic even-degree model. In weighted-projective coordinates these are the solutions with X = 1 and Z = 0.

Equations

MazurTorsion.XOneThirteenFiniteField.InfinityDirection = { η : MazurTorsion.XOneThirteenFiniteField.F3 // η ^ 2 = 1 }

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeInfinityDirection :

Fintype InfinityDirection

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeInfinityDirection = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.infinity_equation_iff_leadingCoeff (η : F3) :

η ^ 2 = 1 ↔ η ^ 2 = sextic.leadingCoeff

The normalized equation η² = 1 is exactly the leading-coefficient equation for this monic sextic.

theorem MazurTorsion.XOneThirteenFiniteField.infinity_direction_satisfies_leadingCoeff (η : InfinityDirection) :

↑η ^ 2 = sextic.leadingCoeff

Every normalized infinity direction satisfies the actual leading-coefficient equation of the sextic.

theorem MazurTorsion.XOneThirteenFiniteField.infinity_direction_iff (η : F3) :

η ^ 2 = 1 ↔ η = 1 ∨ η = -1

The normalized infinity directions are exactly η = ±1.

theorem MazurTorsion.XOneThirteenFiniteField.card_infinityDirection :

Fintype.card InfinityDirection = 2

There are exactly two normalized points in the infinity chart.

theorem MazurTorsion.XOneThirteenFiniteField.infinity_direction_jacobian_nonsingular (η : InfinityDirection) :

2 * ↑η ≠ 0

The Y-partial derivative is nonzero at either infinity direction, so the two normalized infinity-chart points are distinct smooth directions.

def MazurTorsion.XOneThirteenFiniteField.PointCertificate :

The elementary six-element certificate obtained by adjoining the two normalized infinity directions to the four affine solutions.

No equivalence with a projective-curve implementation is claimed here.

Equations

MazurTorsion.XOneThirteenFiniteField.PointCertificate = (MazurTorsion.XOneThirteenFiniteField.AffineSolution ⊕ MazurTorsion.XOneThirteenFiniteField.InfinityDirection)

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificate :

Fintype PointCertificate

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificate = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_pointCertificate :

Fintype.card PointCertificate = 6

The affine enumeration plus the normalized infinity chart has six elements.

The second good prime #

@[reducible, inline]

abbrev MazurTorsion.XOneThirteenFiniteField.F5 :

The five-element residue field used for the second point count.

Equations

MazurTorsion.XOneThirteenFiniteField.F5 = ZMod 5

Instances For

noncomputable def MazurTorsion.XOneThirteenFiniteField.sexticF5 :

The order-thirteen hyperelliptic sextic reduced modulo 5.

Equations

MazurTorsion.XOneThirteenFiniteField.sexticF5 = Polynomial.X ^ 6 + 2 * Polynomial.X ^ 5 + Polynomial.X ^ 4 + 2 * Polynomial.X ^ 3 + 6 * Polynomial.X ^ 2 + 4 * Polynomial.X + 1

Instances For

def MazurTorsion.XOneThirteenFiniteField.sexticValueF5 (x : F5) :

A computable presentation of the sextic's value function modulo 5.

Equations

MazurTorsion.XOneThirteenFiniteField.sexticValueF5 x = x ^ 6 + 2 * x ^ 5 + x ^ 4 + 2 * x ^ 3 + 6 * x ^ 2 + 4 * x + 1

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.eval_sexticF5 (x : F5) :

Polynomial.eval x sexticF5 = sexticValueF5 x

Evaluation of the reduced sextic modulo 5 agrees with the displayed formula.

theorem MazurTorsion.XOneThirteenFiniteField.derivative_sexticF5 :

Polynomial.derivative sexticF5 = Polynomial.X ^ 5 + 4 * Polynomial.X ^ 3 + Polynomial.X ^ 2 + 2 * Polynomial.X + 4

The formal derivative of the sextic modulo 5.

noncomputable def MazurTorsion.XOneThirteenFiniteField.bezoutLeftF5 :

Left Bézout coefficient for the sextic modulo 5 and its derivative.

Equations

MazurTorsion.XOneThirteenFiniteField.bezoutLeftF5 = -Polynomial.X ^ 3 + Polynomial.X ^ 2 - 2 * Polynomial.X + 2

Instances For

noncomputable def MazurTorsion.XOneThirteenFiniteField.bezoutRightF5 :

Right Bézout coefficient for the sextic modulo 5 and its derivative.

Equations

MazurTorsion.XOneThirteenFiniteField.bezoutRightF5 = Polynomial.X ^ 4 + Polynomial.X ^ 3 + 2 * Polynomial.X ^ 2 - 2 * Polynomial.X + 1

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.sexticF5_derivative_bezout :

bezoutLeftF5 * sexticF5 + bezoutRightF5 * Polynomial.derivative sexticF5 = 1

Explicit gcd certificate for the sextic modulo 5 and its derivative.

theorem MazurTorsion.XOneThirteenFiniteField.sexticF5_separable :

sexticF5.Separable

The reduction modulo 5 is separable.

def MazurTorsion.XOneThirteenFiniteField.AffineSolutionF5 :

An affine solution of the reduced equation over 𝔽₅.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeAffineSolutionF5 :

Fintype AffineSolutionF5

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeAffineSolutionF5 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_affineSolutionF5 :

Fintype.card AffineSolutionF5 = 4

There are four affine solutions over 𝔽₅.

def MazurTorsion.XOneThirteenFiniteField.InfinityDirectionF5 :

The normalized infinity directions over 𝔽₅.

Equations

MazurTorsion.XOneThirteenFiniteField.InfinityDirectionF5 = { η : MazurTorsion.XOneThirteenFiniteField.F5 // η ^ 2 = 1 }

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeInfinityDirectionF5 :

Fintype InfinityDirectionF5

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeInfinityDirectionF5 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_infinityDirectionF5 :

Fintype.card InfinityDirectionF5 = 2

There are two normalized infinity directions over 𝔽₅.

def MazurTorsion.XOneThirteenFiniteField.PointCertificateF5 :

The six-element point certificate over 𝔽₅.

Equations

MazurTorsion.XOneThirteenFiniteField.PointCertificateF5 = (MazurTorsion.XOneThirteenFiniteField.AffineSolutionF5 ⊕ MazurTorsion.XOneThirteenFiniteField.InfinityDirectionF5)

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificateF5 :

Fintype PointCertificateF5

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificateF5 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_pointCertificateF5 :

Fintype.card PointCertificateF5 = 6

The affine enumeration and infinity chart have six elements over 𝔽₅.

Quadratic extension certificates #

@[reducible, inline]

abbrev MazurTorsion.XOneThirteenFiniteField.QuadraticPair (n : ℕ) :

A transparent pair presentation of a quadratic algebra over ZMod n. Multiplication below imposes ω² = d.

Equations

MazurTorsion.XOneThirteenFiniteField.QuadraticPair n = (ZMod n × ZMod n)

Instances For

def MazurTorsion.XOneThirteenFiniteField.quadraticPairZero {n : ℕ} :

QuadraticPair n

Zero in the pair presentation.

Equations

MazurTorsion.XOneThirteenFiniteField.quadraticPairZero = (0, 0)

Instances For

def MazurTorsion.XOneThirteenFiniteField.quadraticPairOne {n : ℕ} :

QuadraticPair n

One in the pair presentation.

Equations

MazurTorsion.XOneThirteenFiniteField.quadraticPairOne = (1, 0)

Instances For

def MazurTorsion.XOneThirteenFiniteField.quadraticPairAdd {n : ℕ} (u v : QuadraticPair n) :

QuadraticPair n

Addition in the pair presentation.

Equations

MazurTorsion.XOneThirteenFiniteField.quadraticPairAdd u v = (u.1 + v.1, u.2 + v.2)

Instances For

def MazurTorsion.XOneThirteenFiniteField.quadraticPairMul {n : ℕ} (d : ZMod n) (u v : QuadraticPair n) :

QuadraticPair n

Multiplication in the pair presentation with ω² = d.

Equations

MazurTorsion.XOneThirteenFiniteField.quadraticPairMul d u v = (u.1 * v.1 + d * u.2 * v.2, u.1 * v.2 + u.2 * v.1)

Instances For

def MazurTorsion.XOneThirteenFiniteField.quadraticPairNatScale {n : ℕ} (a : ℕ) (u : QuadraticPair n) :

QuadraticPair n

Natural-number scalar multiplication in the pair presentation.

Equations

MazurTorsion.XOneThirteenFiniteField.quadraticPairNatScale a u = (↑a * u.1, ↑a * u.2)

Instances For

def MazurTorsion.XOneThirteenFiniteField.quadraticPairPow {n : ℕ} (d : ZMod n) (u : QuadraticPair n) :

ℕ → QuadraticPair n

Powers computed with the transparent quadratic multiplication.

Equations

Instances For

def MazurTorsion.XOneThirteenFiniteField.quadraticPairSexticValue {n : ℕ} (d : ZMod n) (x : QuadraticPair n) :

QuadraticPair n

The sextic value in the pair presentation.

Equations

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

Instances For

def MazurTorsion.XOneThirteenFiniteField.QuadraticAffineSolution (n : ℕ) (d : ZMod n) :

A quadratic-pair affine solution.

Equations

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

Instances For

def MazurTorsion.XOneThirteenFiniteField.QuadraticInfinityDirection (n : ℕ) (d : ZMod n) :

A normalized quadratic-pair infinity direction.

Equations

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

Instances For

@[reducible, inline]

abbrev MazurTorsion.XOneThirteenFiniteField.F9Pair :

The pair presentation of 𝔽₉, using ω² = 2.

Equations

MazurTorsion.XOneThirteenFiniteField.F9Pair = MazurTorsion.XOneThirteenFiniteField.QuadraticPair 3

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.two_not_square_F3 (a : F3) :

a ^ 2 ≠ 2

Two is not a square in 𝔽₃.

theorem MazurTorsion.XOneThirteenFiniteField.F9Pair_nonzero_has_mul_inverse (u : F9Pair) :

u ≠ quadraticPairZero → ∃ (v : F9Pair), quadraticPairMul 2 u v = quadraticPairOne

Every nonzero element in the nine-element pair presentation has a multiplicative inverse. Together with two_not_square_F3, this is a finite certificate that the displayed quadratic algebra is the field 𝔽₉.

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticAffineSolutionOfNatNatF3 :

Fintype (QuadraticAffineSolution 3 2)

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticAffineSolutionOfNatNatF3 = id (id inferInstance)

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticInfinityDirectionOfNatNatF3 :

Fintype (QuadraticInfinityDirection 3 2)

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticInfinityDirectionOfNatNatF3 = id (id inferInstance)

theorem MazurTorsion.XOneThirteenFiniteField.card_affineSolutionF9 :

Fintype.card (QuadraticAffineSolution 3 2) = 6

There are six affine solutions over the checked 𝔽₉ presentation.

theorem MazurTorsion.XOneThirteenFiniteField.card_infinityDirectionF9 :

Fintype.card (QuadraticInfinityDirection 3 2) = 2

There are two normalized infinity directions over the checked 𝔽₉ presentation.

def MazurTorsion.XOneThirteenFiniteField.PointCertificateF9 :

The point certificate over 𝔽₉.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificateF9 :

Fintype PointCertificateF9

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificateF9 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_pointCertificateF9 :

Fintype.card PointCertificateF9 = 8

The quadratic-extension point certificate has eight elements over 𝔽₉.

@[reducible, inline]

abbrev MazurTorsion.XOneThirteenFiniteField.F25Pair :

The pair presentation of 𝔽₂₅, using ω² = 2.

Equations

MazurTorsion.XOneThirteenFiniteField.F25Pair = MazurTorsion.XOneThirteenFiniteField.QuadraticPair 5

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.two_not_square_F5 (a : F5) :

a ^ 2 ≠ 2

Two is not a square in 𝔽₅.

theorem MazurTorsion.XOneThirteenFiniteField.F25Pair_nonzero_has_mul_inverse (u : F25Pair) :

u ≠ quadraticPairZero → ∃ (v : F25Pair), quadraticPairMul 2 u v = quadraticPairOne

Every nonzero element in the twenty-five-element pair presentation has a multiplicative inverse.

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticAffineSolutionOfNatNatF5 :

Fintype (QuadraticAffineSolution 5 2)

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticAffineSolutionOfNatNatF5 = id (id inferInstance)

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticInfinityDirectionOfNatNatF5 :

Fintype (QuadraticInfinityDirection 5 2)

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticInfinityDirectionOfNatNatF5 = id (id inferInstance)

theorem MazurTorsion.XOneThirteenFiniteField.card_affineSolutionF25 :

Fintype.card (QuadraticAffineSolution 5 2) = 10

There are ten affine solutions over the checked 𝔽₂₅ presentation.

theorem MazurTorsion.XOneThirteenFiniteField.card_infinityDirectionF25 :

Fintype.card (QuadraticInfinityDirection 5 2) = 2

There are two normalized infinity directions over the checked 𝔽₂₅ presentation.

def MazurTorsion.XOneThirteenFiniteField.PointCertificateF25 :

The point certificate over 𝔽₂₅.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificateF25 :

Fintype PointCertificateF25

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypePointCertificateF25 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_pointCertificateF25 :

Fintype.card PointCertificateF25 = 12

The quadratic-extension point certificate has twelve elements over 𝔽₂₅.

theorem MazurTorsion.XOneThirteenFiniteField.twoPrime_pointCertificate_counts :

(Fintype.card PointCertificate = 6 ∧ Fintype.card PointCertificateF9 = 8) ∧ Fintype.card PointCertificateF5 = 6 ∧ Fintype.card PointCertificateF25 = 12

The two checked pairs of point counts. For a smooth projective genus-two curve these are the inputs (#C(𝔽_q), #C(𝔽_{q²})) to the standard Jacobian-order formula. This theorem only packages the finite enumerations; it does not supply that geometric identification.

Degree-two divisor labels #

inductive MazurTorsion.XOneThirteenFiniteField.RationalCuspLabel :

Labels for the six rational cusp points in either good reduction.

zeroPos : RationalCuspLabel
zeroNeg : RationalCuspLabel
negOnePos : RationalCuspLabel
negOneNeg : RationalCuspLabel
infinityPos : RationalCuspLabel
infinityNeg : RationalCuspLabel

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instDecidableEqRationalCuspLabel :

DecidableEq RationalCuspLabel

Equations

MazurTorsion.XOneThirteenFiniteField.instDecidableEqRationalCuspLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeRationalCuspLabel :

Fintype RationalCuspLabel

Equations

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

def MazurTorsion.XOneThirteenFiniteField.rationalCuspLabelIndex :

RationalCuspLabel → Fin 6

The ordering used to give unordered pairs a unique representative.

Equations

Instances For

def MazurTorsion.XOneThirteenFiniteField.rationalCuspConjugate :

RationalCuspLabel → RationalCuspLabel

The hyperelliptic involution on rational cusp labels.

Equations

Instances For

def MazurTorsion.XOneThirteenFiniteField.rationalCuspLabelPointF3 :

RationalCuspLabel → PointCertificate

The cusp label interpreted in the point certificate over 𝔽₃.

Equations

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

Instances For

def MazurTorsion.XOneThirteenFiniteField.pointCertificateCuspLabelF3 :

PointCertificate → RationalCuspLabel

A computational inverse label for the 𝔽₃ point certificate.

Equations

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

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.pointCertificateCuspLabelF3_leftInverse :

Function.LeftInverse pointCertificateCuspLabelF3 rationalCuspLabelPointF3

The inverse label recovers every rational cusp label over 𝔽₃.

theorem MazurTorsion.XOneThirteenFiniteField.rationalCuspLabelPointF3_bijective :

Function.Bijective rationalCuspLabelPointF3

The six cusp labels enumerate the complete point certificate over 𝔽₃.

def MazurTorsion.XOneThirteenFiniteField.rationalCuspLabelPointF5 :

RationalCuspLabel → PointCertificateF5

The cusp label interpreted in the point certificate over 𝔽₅.

Equations

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

Instances For

def MazurTorsion.XOneThirteenFiniteField.pointCertificateCuspLabelF5 :

PointCertificateF5 → RationalCuspLabel

A computational inverse label for the 𝔽₅ point certificate.

Equations

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

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.pointCertificateCuspLabelF5_leftInverse :

Function.LeftInverse pointCertificateCuspLabelF5 rationalCuspLabelPointF5

The inverse label recovers every rational cusp label over 𝔽₅.

theorem MazurTorsion.XOneThirteenFiniteField.rationalCuspLabelPointF5_bijective :

Function.Bijective rationalCuspLabelPointF5

The six cusp labels enumerate the complete point certificate over 𝔽₅.

def MazurTorsion.XOneThirteenFiniteField.UnorderedRationalCuspPair :

An unordered pair of rational cusp labels, represented in increasing index order.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeUnorderedRationalCuspPair :

Fintype UnorderedRationalCuspPair

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeUnorderedRationalCuspPair = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_unorderedRationalCuspPair :

Fintype.card UnorderedRationalCuspPair = 21

Six points have twenty-one unordered pairs with repetition.

def MazurTorsion.XOneThirteenFiniteField.IsRationalHyperellipticPair (p : UnorderedRationalCuspPair) :

A rational cusp pair is a member of the hyperelliptic pencil when its second label is the conjugate of its first.

Equations

MazurTorsion.XOneThirteenFiniteField.IsRationalHyperellipticPair p = ((↑p).2 = MazurTorsion.XOneThirteenFiniteField.rationalCuspConjugate (↑p).1)

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instDecidableIsRationalHyperellipticPair (p : UnorderedRationalCuspPair) :

Decidable (IsRationalHyperellipticPair p)

Equations

MazurTorsion.XOneThirteenFiniteField.instDecidableIsRationalHyperellipticPair p = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_rationalHyperellipticPair :

Fintype.card { p : UnorderedRationalCuspPair // IsRationalHyperellipticPair p } = 3

Exactly three rational unordered pairs are hyperelliptic fibers.

def MazurTorsion.XOneThirteenFiniteField.quadraticPairConjugate {n : ℕ} (u : QuadraticPair n) :

QuadraticPair n

Conjugation in the pair presentation.

Equations

MazurTorsion.XOneThirteenFiniteField.quadraticPairConjugate u = (u.1, -u.2)

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.quadraticPairPow_three_eq_conjugate_F9 (u : F9Pair) :

quadraticPairPow 2 u 3 = quadraticPairConjugate u

Cubing in the checked nine-element presentation is pair conjugation.

theorem MazurTorsion.XOneThirteenFiniteField.quadraticPairPow_five_eq_conjugate_F25 (u : F25Pair) :

quadraticPairPow 2 u 5 = quadraticPairConjugate u

Fifth powering in the checked twenty-five-element presentation is pair conjugation.

def MazurTorsion.XOneThirteenFiniteField.IsNonBaseQuadraticAffineSolution {n : ℕ} {d : ZMod n} (P : QuadraticAffineSolution n d) :

A quadratic affine solution whose two coordinates do not both lie in the base field.

Equations

MazurTorsion.XOneThirteenFiniteField.IsNonBaseQuadraticAffineSolution P = ((↑P).1.2 ≠ 0 ∨ (↑P).2.2 ≠ 0)

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instDecidableIsNonBaseQuadraticAffineSolution {n : ℕ} {d : ZMod n} (P : QuadraticAffineSolution n d) :

Decidable (IsNonBaseQuadraticAffineSolution P)

Equations

MazurTorsion.XOneThirteenFiniteField.instDecidableIsNonBaseQuadraticAffineSolution P = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_nonBaseAffineSolutionF9 :

Fintype.card { P : QuadraticAffineSolution 3 2 // IsNonBaseQuadraticAffineSolution P } = 2

There are two non-base affine solutions over 𝔽₉.

theorem MazurTorsion.XOneThirteenFiniteField.nonBaseAffineSolutionF9_abscissa (P : QuadraticAffineSolution 3 2) :

IsNonBaseQuadraticAffineSolution P → (↑P).1 = (1, 0) ∧ (↑P).2.2 ≠ 0

The non-base 𝔽₉ solutions form the fiber above the base-field abscissa 1, and their ordinates are genuinely quadratic.

theorem MazurTorsion.XOneThirteenFiniteField.nonBaseAffineSolutionF9_ordinates (P Q : QuadraticAffineSolution 3 2) :

IsNonBaseQuadraticAffineSolution P → IsNonBaseQuadraticAffineSolution Q → (↑P).1 = (↑Q).1 → (↑Q).2 = (↑P).2 ∨ (↑Q).2 = quadraticPairConjugate (↑P).2

At the non-base 𝔽₉ abscissa, the two ordinates are equal or quadratic conjugates.

theorem MazurTorsion.XOneThirteenFiniteField.card_nonBaseAffineSolutionF25 :

Fintype.card { P : QuadraticAffineSolution 5 2 // IsNonBaseQuadraticAffineSolution P } = 6

There are six non-base affine solutions over 𝔽₂₅.

theorem MazurTorsion.XOneThirteenFiniteField.nonBaseAffineSolutionF25_abscissa (P : QuadraticAffineSolution 5 2) :

IsNonBaseQuadraticAffineSolution P → (↑P).1.2 = 0 ∧ ((↑P).1.1 = 1 ∨ (↑P).1.1 = 2 ∨ (↑P).1.1 = 3) ∧ (↑P).2.2 ≠ 0

The non-base 𝔽₂₅ solutions lie above the three base-field abscissas 1, 2, and 3, with genuinely quadratic ordinates.

theorem MazurTorsion.XOneThirteenFiniteField.nonBaseAffineSolutionF25_ordinates (P Q : QuadraticAffineSolution 5 2) :

IsNonBaseQuadraticAffineSolution P → IsNonBaseQuadraticAffineSolution Q → (↑P).1 = (↑Q).1 → (↑Q).2 = (↑P).2 ∨ (↑Q).2 = quadraticPairConjugate (↑P).2

Above any of the three non-base 𝔽₂₅ abscissas, the two ordinates are equal or quadratic conjugates.

def MazurTorsion.XOneThirteenFiniteField.QuadraticClosedFiberF3 :

The one quadratic closed fiber over 𝔽₃, labeled by its base-field abscissa.

Equations

MazurTorsion.XOneThirteenFiniteField.QuadraticClosedFiberF3 = { x : MazurTorsion.XOneThirteenFiniteField.F3 // x = 1 }

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticClosedFiberF3 :

Fintype QuadraticClosedFiberF3

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticClosedFiberF3 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_quadraticClosedFiberF3 :

Fintype.card QuadraticClosedFiberF3 = 1

There is one non-rational quadratic closed fiber over 𝔽₃.

def MazurTorsion.XOneThirteenFiniteField.QuadraticClosedFiberF5 :

The three quadratic closed fibers over 𝔽₅, labeled by their base-field abscissas.

Equations

MazurTorsion.XOneThirteenFiniteField.QuadraticClosedFiberF5 = { x : MazurTorsion.XOneThirteenFiniteField.F5 // x = 1 ∨ x = 2 ∨ x = 3 }

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticClosedFiberF5 :

Fintype QuadraticClosedFiberF5

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeQuadraticClosedFiberF5 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_quadraticClosedFiberF5 :

Fintype.card QuadraticClosedFiberF5 = 3

There are three non-rational quadratic closed fibers over 𝔽₅.

def MazurTorsion.XOneThirteenFiniteField.DegreeTwoDivisorCertificateF3 :

Degree-two effective-divisor labels over 𝔽₃: either an unordered pair of rational points or the unique quadratic Frobenius orbit.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeDegreeTwoDivisorCertificateF3 :

Fintype DegreeTwoDivisorCertificateF3

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeDegreeTwoDivisorCertificateF3 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_degreeTwoDivisorCertificateF3 :

Fintype.card DegreeTwoDivisorCertificateF3 = 22

The degree-two certificate over 𝔽₃ has twenty-two elements.

def MazurTorsion.XOneThirteenFiniteField.DegreeTwoDivisorCertificateF5 :

Degree-two effective-divisor labels over 𝔽₅.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeDegreeTwoDivisorCertificateF5 :

Fintype DegreeTwoDivisorCertificateF5

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeDegreeTwoDivisorCertificateF5 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_degreeTwoDivisorCertificateF5 :

Fintype.card DegreeTwoDivisorCertificateF5 = 24

The degree-two certificate over 𝔽₅ has twenty-four elements.

def MazurTorsion.XOneThirteenFiniteField.IsCanonicalDegreeTwoF3 :

DegreeTwoDivisorCertificateF3 → Prop

The hyperelliptic-pencil labels among the degree-two certificates over 𝔽₃. The quadratic closed fiber is one of those pencil members.

Equations

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instDecidableIsCanonicalDegreeTwoF3 (D : DegreeTwoDivisorCertificateF3) :

Decidable (IsCanonicalDegreeTwoF3 D)

Equations

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

theorem MazurTorsion.XOneThirteenFiniteField.card_canonicalDegreeTwoF3 :

Fintype.card { D : DegreeTwoDivisorCertificateF3 // IsCanonicalDegreeTwoF3 D } = 4

The hyperelliptic pencil has four labels over 𝔽₃.

def MazurTorsion.XOneThirteenFiniteField.IsCanonicalDegreeTwoF5 :

DegreeTwoDivisorCertificateF5 → Prop

The hyperelliptic-pencil labels over 𝔽₅.

Equations

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instDecidableIsCanonicalDegreeTwoF5 (D : DegreeTwoDivisorCertificateF5) :

Decidable (IsCanonicalDegreeTwoF5 D)

Equations

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

theorem MazurTorsion.XOneThirteenFiniteField.card_canonicalDegreeTwoF5 :

Fintype.card { D : DegreeTwoDivisorCertificateF5 // IsCanonicalDegreeTwoF5 D } = 6

The hyperelliptic pencil has six labels over 𝔽₅.

def MazurTorsion.XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF3 :

The combinatorial reduced degree-two class certificate over 𝔽₃: retain every noncanonical divisor label and collapse the complete hyperelliptic pencil to one distinguished label.

This is not defined to be a Picard group or a Jacobian.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeReducedDegreeTwoClassCertificateF3 :

Fintype ReducedDegreeTwoClassCertificateF3

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeReducedDegreeTwoClassCertificateF3 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_reducedDegreeTwoClassCertificateF3 :

Fintype.card ReducedDegreeTwoClassCertificateF3 = 19

The reduced degree-two class certificate over 𝔽₃ has nineteen elements.

def MazurTorsion.XOneThirteenFiniteField.ReducedDegreeTwoClassCertificateF5 :

The analogous combinatorial reduced degree-two class certificate over 𝔽₅. No Picard or Jacobian identification is asserted.

Equations

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

Instances For

@[instance_reducible]

instance MazurTorsion.XOneThirteenFiniteField.instFintypeReducedDegreeTwoClassCertificateF5 :

Fintype ReducedDegreeTwoClassCertificateF5

Equations

MazurTorsion.XOneThirteenFiniteField.instFintypeReducedDegreeTwoClassCertificateF5 = id inferInstance

theorem MazurTorsion.XOneThirteenFiniteField.card_reducedDegreeTwoClassCertificateF5 :

Fintype.card ReducedDegreeTwoClassCertificateF5 = 19

The reduced degree-two class certificate over 𝔽₅ has nineteen elements.

A cyclic coordinate on the reduced class certificates #

def MazurTorsion.XOneThirteenFiniteField.rationalCuspDegreeTwoCoordinate :

RationalCuspLabel → ZMod 19

A perfect six-element degree-two coordinate set in ZMod 19. Opposite labels are hyperelliptic conjugates.

Equations

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.rationalCuspDegreeTwoCoordinate_conjugate (c : RationalCuspLabel) :

rationalCuspDegreeTwoCoordinate (rationalCuspConjugate c) = -rationalCuspDegreeTwoCoordinate c

Hyperelliptic conjugation negates the cusp coordinate.

def MazurTorsion.XOneThirteenFiniteField.unorderedRationalCuspPairCoordinate (p : UnorderedRationalCuspPair) :

The coordinate of an unordered rational cusp pair.

Equations

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

Instances For

def MazurTorsion.XOneThirteenFiniteField.degreeTwoClassCoordinateF3 :

DegreeTwoDivisorCertificateF3 → ZMod 19

The degree-two class coordinate over 𝔽₃. A quadratic hyperelliptic fiber has coordinate zero.

Equations

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.degreeTwoClassCoordinateF3_eq_zero_iff (D : DegreeTwoDivisorCertificateF3) :

degreeTwoClassCoordinateF3 D = 0 ↔ IsCanonicalDegreeTwoF3 D

Vanishing of the 𝔽₃ coordinate detects exactly the canonical hyperelliptic pencil.

def MazurTorsion.XOneThirteenFiniteField.degreeTwoClassCoordinateF5 :

DegreeTwoDivisorCertificateF5 → ZMod 19

The degree-two class coordinate over 𝔽₅.

Equations

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.degreeTwoClassCoordinateF5_eq_zero_iff (D : DegreeTwoDivisorCertificateF5) :

degreeTwoClassCoordinateF5 D = 0 ↔ IsCanonicalDegreeTwoF5 D

Vanishing of the 𝔽₅ coordinate detects exactly the canonical hyperelliptic pencil.

def MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassCoordinateF3 :

ReducedDegreeTwoClassCertificateF3 → ZMod 19

The reduced coordinate over 𝔽₃; the collapsed pencil is sent to zero and every noncanonical divisor retains its nonzero coordinate.

Equations

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassCoordinateF3_bijective :

Function.Bijective reducedDegreeTwoClassCoordinateF3

The reduced coordinate over 𝔽₃ is a bijection.

noncomputable def MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassEquivZModF3 :

ReducedDegreeTwoClassCertificateF3 ≃ ZMod 19

The checked equivalence between the reduced 𝔽₃ certificate and the nineteen cyclic coordinates.

Equations

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

Instances For

@[instance_reducible]

noncomputable instance MazurTorsion.XOneThirteenFiniteField.instAddCommGroupReducedDegreeTwoClassCertificateF3 :

AddCommGroup ReducedDegreeTwoClassCertificateF3

Transport the cyclic group law along the checked 𝔽₃ coordinate. This is a group law on the combinatorial certificate, not an assertion that it is the geometric Jacobian.

Equations

MazurTorsion.XOneThirteenFiniteField.instAddCommGroupReducedDegreeTwoClassCertificateF3 = MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassEquivZModF3.addCommGroup

noncomputable def MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassAddEquivZModF3 :

ReducedDegreeTwoClassCertificateF3 ≃+ ZMod 19

With the transported group law, the coordinate is an additive equivalence to ZMod 19.

Equations

MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassAddEquivZModF3 = MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassEquivZModF3.addEquiv

Instances For

def MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassCoordinateF5 :

ReducedDegreeTwoClassCertificateF5 → ZMod 19

The reduced coordinate over 𝔽₅.

Equations

Instances For

theorem MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassCoordinateF5_bijective :

Function.Bijective reducedDegreeTwoClassCoordinateF5

The reduced coordinate over 𝔽₅ is a bijection.

noncomputable def MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassEquivZModF5 :

ReducedDegreeTwoClassCertificateF5 ≃ ZMod 19

The checked equivalence between the reduced 𝔽₅ certificate and ZMod 19.

Equations

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

Instances For

@[instance_reducible]

noncomputable instance MazurTorsion.XOneThirteenFiniteField.instAddCommGroupReducedDegreeTwoClassCertificateF5 :

AddCommGroup ReducedDegreeTwoClassCertificateF5

The transported cyclic group law on the 𝔽₅ certificate.

Equations

MazurTorsion.XOneThirteenFiniteField.instAddCommGroupReducedDegreeTwoClassCertificateF5 = MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassEquivZModF5.addCommGroup

noncomputable def MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassAddEquivZModF5 :

ReducedDegreeTwoClassCertificateF5 ≃+ ZMod 19

The additive cyclic coordinate over 𝔽₅.

Equations

MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassAddEquivZModF5 = MazurTorsion.XOneThirteenFiniteField.reducedDegreeTwoClassEquivZModF5.addEquiv

Instances For