The explicit first seven-isogeny on the order-seven Tate family

For the order-seven Tate family, the six nonzero points in the marked subgroup have abscissae 0, b, and c, each occurring twice. Pairing opposite points in Vélu's formula gives a compact rational map with three double poles. This file records that formula, verifies that it lands on the explicit quotient model, and treats all kernel poles as points at infinity.

The map is deliberately kept as an underlying point function. Compatibility with addition, or just with multiplication by seven, is a separate theorem needed by the order-49 tower.

def MazurTorsion.Kubert.orderSevenB (d : ℚ) : ℚ

The b parameter of the order-seven Tate family.

Equations

• MazurTorsion.Kubert.orderSevenB d = d ^ 3 - d ^ 2

def MazurTorsion.Kubert.orderSevenC (d : ℚ) : ℚ

The c parameter of the order-seven Tate family.

Equations

• MazurTorsion.Kubert.orderSevenC d = d ^ 2 - d

def MazurTorsion.Kubert.orderSevenFamily (d : ℚ) : WeierstrassCurve ℚ

The order-seven Tate family, with marked point (0,0).

Equations

• MazurTorsion.Kubert.orderSevenFamily d = MazurTorsion.Kubert.tateNormalCurve (MazurTorsion.Kubert.orderSevenB d) (MazurTorsion.Kubert.orderSevenC d)

def MazurTorsion.Kubert.orderSevenQuotient (d : ℚ) : WeierstrassCurve ℚ

The normalized coefficient model produced by Vélu's formula for the quotient by the marked order-seven subgroup.

Equations

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

theorem MazurTorsion.Kubert.orderSevenFamily_Δ (d : ℚ) : (orderSevenFamily d).Δ = d ^ 7 * (d - 1) ^ 7 * (d ^ 3 - 8 * d ^ 2 + 5 * d + 1)

The discriminant of the source order-seven family.

theorem MazurTorsion.Kubert.orderSevenQuotient_Δ (d : ℚ) : (orderSevenQuotient d).Δ = d * (d - 1) * (d ^ 3 - 8 * d ^ 2 + 5 * d + 1) ^ 7

The discriminant of the marked order-seven quotient model.

theorem MazurTorsion.Kubert.orderSevenQuotient_c₄ (d : ℚ) : (orderSevenQuotient d).c₄ = (d ^ 2 - d + 1) * (d ^ 6 + 229 * d ^ 5 + 270 * d ^ 4 - 1695 * d ^ 3 + 1430 * d ^ 2 - 235 * d + 1)

The c₄ invariant of the marked order-seven quotient model.

def MazurTorsion.Kubert.orderSevenFrickeParameter (d : ℚ) : ℚ

The Fricke/backtracking Hauptmodul on the quotient family. It is 49 / t₇ for the source-family Hauptmodul.

Equations

• MazurTorsion.Kubert.orderSevenFrickeParameter d = (d ^ 3 - 8 * d ^ 2 + 5 * d + 1) / (d * (d - 1))

theorem MazurTorsion.Kubert.orderSevenQuotient_hauptmodul_identity (d : ℚ) (hd0 : d ≠ 0) (hd1 : d ≠ 1) : orderSevenJNumerator (orderSevenFrickeParameter d) * (orderSevenQuotient d).Δ = (orderSevenQuotient d).c₄ ^ 3 * orderSevenFrickeParameter d ^ 7

The quotient invariants satisfy the level-seven Hauptmodul identity for the Fricke/backtracking parameter.

instance MazurTorsion.Kubert.orderSevenQuotient_isElliptic (d : ℚ) [(orderSevenFamily d).IsElliptic] : (orderSevenQuotient d).IsElliptic

Nonsingularity of the source family implies nonsingularity of its explicit order-seven quotient model.

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

The abscissa of the explicit Vélu map away from its three kernel abscissae.

Equations

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

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

The rational differential factor of the explicit Vélu abscissa.

Equations

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

def MazurTorsion.Kubert.orderSevenVeluY (d x y : ℚ) : ℚ

The ordinate of the explicit Vélu map, normalized to preserve the invariant differential.

Equations

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

theorem MazurTorsion.Kubert.orderSevenVelu_completedY (d x y : ℚ) : 2 * orderSevenVeluY d x y + (orderSevenQuotient d).a₁ * orderSevenVeluX d x + (orderSevenQuotient d).a₃ = orderSevenVeluDifferential d x * (2 * y + (orderSevenFamily d).a₁ * x + (orderSevenFamily d).a₃)

The completed ordinate of the Vélu image is the source completed ordinate multiplied by the explicit differential factor.

def MazurTorsion.Kubert.orderSevenResidualHauptmodul (d x y : ℚ) : ℚ

The residual level-seven Hauptmodul obtained by applying explicit Tate normalization to the Vélu image of an affine source point.

Equations

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

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

The kernel polynomial whose roots are the three affine pole abscissae.

Equations

• MazurTorsion.Kubert.orderSevenKernelPolynomial d x = x * (x - MazurTorsion.Kubert.orderSevenB d) * (x - MazurTorsion.Kubert.orderSevenC d)

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

The cleared numerator of orderSevenVeluX; its denominator is the square of orderSevenKernelPolynomial.

Equations

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

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

The cleared numerator of orderSevenVeluDifferential; its denominator is the cube of orderSevenKernelPolynomial.

Equations

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

theorem MazurTorsion.Kubert.orderSevenVeluX_eq_div {d x : ℚ} (hx0 : x ≠ 0) (hxb : x ≠ orderSevenB d) (hxc : x ≠ orderSevenC d) : orderSevenVeluX d x = orderSevenVeluXNumerator d x / orderSevenKernelPolynomial d x ^ 2

Away from the kernel abscissae, the explicit Vélu abscissa is the cleared numerator divided by the square of the kernel polynomial.

theorem MazurTorsion.Kubert.orderSevenVeluDifferential_eq_div {d x : ℚ} (hx0 : x ≠ 0) (hxb : x ≠ orderSevenB d) (hxc : x ≠ orderSevenC d) : orderSevenVeluDifferential d x = orderSevenVeluDifferentialNumerator d x / orderSevenKernelPolynomial d x ^ 3

Away from the kernel abscissae, the explicit Vélu differential is the cleared numerator divided by the cube of the kernel polynomial.

theorem MazurTorsion.Kubert.orderSevenVelu_completedSquare {d x : ℚ} (hx0 : x ≠ 0) (hxb : x ≠ orderSevenB d) (hxc : x ≠ orderSevenC d) : orderSevenVeluDifferential d x ^ 2 * (4 * x ^ 3 + (orderSevenFamily d).b₂ * x ^ 2 + 2 * (orderSevenFamily d).b₄ * x + (orderSevenFamily d).b₆) = 4 * orderSevenVeluX d x ^ 3 + (orderSevenQuotient d).b₂ * orderSevenVeluX d x ^ 2 + 2 * (orderSevenQuotient d).b₄ * orderSevenVeluX d x + (orderSevenQuotient d).b₆

The completed-square cubic identity behind the explicit Vélu map.

theorem MazurTorsion.Kubert.orderSevenVelu_equation {d x y : ℚ} (hcurve : (orderSevenFamily d).toAffine.Equation x y) (hx0 : x ≠ 0) (hxb : x ≠ orderSevenB d) (hxc : x ≠ orderSevenC d) : (orderSevenQuotient d).toAffine.Equation (orderSevenVeluX d x) (orderSevenVeluY d x y)

Away from the three kernel abscissae, the explicit Vélu functions carry the source affine equation to the quotient affine equation.

def MazurTorsion.Kubert.OrderSevenKernelX (d x : ℚ) : Prop

The three affine pole abscissae of the order-seven Vélu map.

Equations

• MazurTorsion.Kubert.OrderSevenKernelX d x = (x = 0 ∨ x = MazurTorsion.Kubert.orderSevenB d ∨ x = MazurTorsion.Kubert.orderSevenC d)

@[instance_reducible]

instance MazurTorsion.Kubert.orderSevenKernelXDecidable (d x : ℚ) : Decidable (OrderSevenKernelX d x)

Equations

• MazurTorsion.Kubert.orderSevenKernelXDecidable d x = id inferInstance

theorem MazurTorsion.Kubert.orderSevenOrigin_nonsingular (d : ℚ) [(orderSevenFamily d).IsElliptic] : (orderSevenFamily d).toAffine.Nonsingular 0 0

The marked origin is nonsingular on every nonsingular member of the order-seven family.

noncomputable def MazurTorsion.Kubert.orderSevenOrigin (d : ℚ) [(orderSevenFamily d).IsElliptic] : (orderSevenFamily d).toAffine.Point

The marked order-seven point (0,0) on the source family.

Equations

• MazurTorsion.Kubert.orderSevenOrigin d = WeierstrassCurve.Affine.Point.some 0 0 ⋯

theorem MazurTorsion.Kubert.orderSevenFamily_parameters_ne (d : ℚ) [(orderSevenFamily d).IsElliptic] : d ≠ 0 ∧ d ≠ 1 ∧ d ^ 3 - 8 * d ^ 2 + 5 * d + 1 ≠ 0

Nonsingularity excludes the three bad parameters of the order-seven family.

theorem MazurTorsion.Kubert.orderSevenFrickeParameter_ne_zero (d : ℚ) [(orderSevenFamily d).IsElliptic] : orderSevenFrickeParameter d ≠ 0

The Fricke/backtracking Hauptmodul is nonzero on every nonsingular member of the source family.

@[simp]

theorem MazurTorsion.Kubert.seven_nsmul_orderSevenOrigin (d : ℚ) [(orderSevenFamily d).IsElliptic] : 7 • orderSevenOrigin d = 0

The marked origin is killed by seven on the parametrized family.

theorem MazurTorsion.Kubert.addOrderOf_orderSevenOrigin (d : ℚ) [(orderSevenFamily d).IsElliptic] : addOrderOf (orderSevenOrigin d) = 7

The marked origin has exact additive order seven.

noncomputable def MazurTorsion.Kubert.orderSevenVeluPoint {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (hx0 : x ≠ 0) (hxb : x ≠ orderSevenB d) (hxc : x ≠ orderSevenC d) : (orderSevenQuotient d).toAffine.Point

The denominator-safe affine value of the explicit Vélu map.

Equations

• MazurTorsion.Kubert.orderSevenVeluPoint hP hx0 hxb hxc = WeierstrassCurve.Affine.Point.some (MazurTorsion.Kubert.orderSevenVeluX d x) (MazurTorsion.Kubert.orderSevenVeluY d x y) ⋯

theorem MazurTorsion.Kubert.orderSevenVeluPoint_add_origin {d x y x' y' : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (hP' : (orderSevenFamily d).toAffine.Nonsingular x' y') (hadd : WeierstrassCurve.Affine.Point.some x y hP + orderSevenOrigin d = WeierstrassCurve.Affine.Point.some x' y' hP') (hx0 : x ≠ 0) (hxb : x ≠ orderSevenB d) (hxc : x ≠ orderSevenC d) (hx0' : x' ≠ 0) (hxb' : x' ≠ orderSevenB d) (hxc' : x' ≠ orderSevenC d) : orderSevenVeluPoint hP' hx0' hxb' hxc' = orderSevenVeluPoint hP hx0 hxb hxc

Away from the kernel poles, the explicit Vélu point is invariant under translation by the marked order-seven point.

noncomputable def MazurTorsion.Kubert.orderSevenPointMap (d : ℚ) [(orderSevenFamily d).IsElliptic] : (orderSevenFamily d).toAffine.Point → (orderSevenQuotient d).toAffine.Point

The total explicit Vélu point function. The point at infinity and the six affine kernel points are sent to infinity.

Equations

• One or more equations did not get rendered due to their size.
• MazurTorsion.Kubert.orderSevenPointMap d WeierstrassCurve.Affine.Point.zero = 0

@[simp]

theorem MazurTorsion.Kubert.orderSevenPointMap_zero (d : ℚ) [(orderSevenFamily d).IsElliptic] : orderSevenPointMap d 0 = 0

theorem MazurTorsion.Kubert.orderSevenPointMap_some_of_not_kernelX {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (hx : ¬OrderSevenKernelX d x) : orderSevenPointMap d (WeierstrassCurve.Affine.Point.some x y hP) = orderSevenVeluPoint hP ⋯ ⋯ ⋯

Evaluation of the total point map away from the kernel poles.

theorem MazurTorsion.Kubert.orderSevenPointMap_some_eq_zero_iff {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) : orderSevenPointMap d (WeierstrassCurve.Affine.Point.some x y hP) = 0 ↔ OrderSevenKernelX d x

An affine point maps to infinity exactly at one of the three kernel abscissae.

@[simp]

theorem MazurTorsion.Kubert.orderSevenPointMap_origin (d : ℚ) [(orderSevenFamily d).IsElliptic] : orderSevenPointMap d (orderSevenOrigin d) = 0

theorem MazurTorsion.Kubert.orderSevenPointMap_add_origin_of_order_fortyNine {d : ℚ} [(orderSevenFamily d).IsElliptic] {Q : (orderSevenFamily d).toAffine.Point} (hQ : addOrderOf Q = 49) : orderSevenPointMap d (Q + orderSevenOrigin d) = orderSevenPointMap d Q

Translation invariance at exact order 49, stated for an arbitrary source point.

theorem MazurTorsion.Kubert.orderSevenPointMap_add_nsmul_origin_of_order_fortyNine {d : ℚ} [(orderSevenFamily d).IsElliptic] {Q : (orderSevenFamily d).toAffine.Point} (hQ : addOrderOf Q = 49) (n : ℕ) : orderSevenPointMap d (Q + n • orderSevenOrigin d) = orderSevenPointMap d Q

Repeated translation by the marked kernel point does not change the explicit image of an exact-order-49 point.

theorem MazurTorsion.Kubert.exists_eq_nsmul_orderSevenOrigin_of_pointMap_eq_zero {d : ℚ} [(orderSevenFamily d).IsElliptic] {R : (orderSevenFamily d).toAffine.Point} (hR : orderSevenPointMap d R = 0) : ∃ n < 7, R = n • orderSevenOrigin d

Every point in the zero fiber is one of the seven multiples of the marked kernel generator.

theorem MazurTorsion.Kubert.orderSevenPointMap_kernel_killed_by_seven {d : ℚ} [(orderSevenFamily d).IsElliptic] {P : (orderSevenFamily d).toAffine.Point} (hP : orderSevenPointMap d P = 0) : 7 • P = 0

Every point in the zero fiber of the explicit Vélu function is killed by seven.

theorem MazurTorsion.Kubert.not_orderSevenKernelX_of_order_fortyNine {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (horder : addOrderOf (WeierstrassCurve.Affine.Point.some x y hP) = 49) : ¬OrderSevenKernelX d x

An affine point of exact order 49 cannot lie in the marked order-seven kernel.

theorem MazurTorsion.Kubert.addOrderOf_orderSevenPointMap_of_order_fortyNine {d : ℚ} [(orderSevenFamily d).IsElliptic] {Q : (orderSevenFamily d).toAffine.Point} (hQ : addOrderOf Q = 49) (hkernel : orderSevenPointMap d (7 • Q) = 0) (hmap : orderSevenPointMap d (7 • Q) = 7 • orderSevenPointMap d Q) : addOrderOf (orderSevenPointMap d Q) = 7

The exact-order consequence needed at the first stage of the order-49 tower. Full additivity of the explicit point function is unnecessary here: it suffices to know compatibility with the single multiple 7 • Q.

theorem MazurTorsion.Kubert.exists_orderSevenHauptmodul_of_order_fortyNine_image {d : ℚ} [(orderSevenFamily d).IsElliptic] {Q : (orderSevenFamily d).toAffine.Point} (hQ : addOrderOf Q = 49) (hkernel : orderSevenPointMap d (7 • Q) = 0) (hmap : orderSevenPointMap d (7 • Q) = 7 • orderSevenPointMap d Q) : ∃ (B : ℚ), B ≠ 0 ∧ orderSevenJNumerator B * (orderSevenQuotient d).Δ = (orderSevenQuotient d).c₄ ^ 3 * B ^ 7

The order-49 image supplies the residual nonzero level-seven Hauptmodul on the quotient. This is the downstream consumer of the generic exact-order-seven normalization theorem.

theorem MazurTorsion.Kubert.orderSevenResidualHauptmodul_spec_of_order_fortyNine {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (hQ : addOrderOf (WeierstrassCurve.Affine.Point.some x y hP) = 49) (hkernel : orderSevenPointMap d (7 • WeierstrassCurve.Affine.Point.some x y hP) = 0) (hmap : orderSevenPointMap d (7 • WeierstrassCurve.Affine.Point.some x y hP) = 7 • orderSevenPointMap d (WeierstrassCurve.Affine.Point.some x y hP)) : orderSevenResidualHauptmodul d x y ≠ 0 ∧ orderSevenJNumerator (orderSevenResidualHauptmodul d x y) * (orderSevenQuotient d).Δ = (orderSevenQuotient d).c₄ ^ 3 * orderSevenResidualHauptmodul d x y ^ 7

For an affine order-49 point, the residual Hauptmodul is the explicit Tate-normalization expression evaluated at its Vélu image.

theorem MazurTorsion.Kubert.orderSevenG7F_eq_zero_of_quotient_hauptmodul {d B : ℚ} [(orderSevenFamily d).IsElliptic] (hoff : orderSevenFrickeParameter d ≠ B) (hB : orderSevenJNumerator B * (orderSevenQuotient d).Δ = (orderSevenQuotient d).c₄ ^ 3 * B ^ 7) : orderSevenG7F (orderSevenFrickeParameter d) B = 0

A second nonbacktracking level-seven Hauptmodul for the quotient gives a point on the level-49 correspondence. This packages the cancellation of the nonzero quotient discriminant; constructing B and proving that it differs from the Fricke/backtracking parameter remain separate tasks.

theorem MazurTorsion.Kubert.orderSevenG7F_residual_eq_zero_of_order_fortyNine {d x y : ℚ} [(orderSevenFamily d).IsElliptic] (hP : (orderSevenFamily d).toAffine.Nonsingular x y) (hQ : addOrderOf (WeierstrassCurve.Affine.Point.some x y hP) = 49) (hkernel : orderSevenPointMap d (7 • WeierstrassCurve.Affine.Point.some x y hP) = 0) (hmap : orderSevenPointMap d (7 • WeierstrassCurve.Affine.Point.some x y hP) = 7 • orderSevenPointMap d (WeierstrassCurve.Affine.Point.some x y hP)) (hoff : orderSevenFrickeParameter d ≠ orderSevenResidualHauptmodul d x y) : orderSevenG7F (orderSevenFrickeParameter d) (orderSevenResidualHauptmodul d x y) = 0

The explicit residual Hauptmodul attached to an affine order-49 point lies on the level-49 correspondence whenever it is not the Fricke/backtracking parameter.