Naïve-height descent for rational elliptic curves

This file is a narrow port of the height part of Michael Stoll's EllipticCurves/MordellWeil.lean, commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

It proves the approximate parallelogram law for the naïve logarithmic height on affine Weierstrass points. Combined with Northcott and finite index of the doubling map, this gives finite generation by AddCommGroup.fg_of_descent'.

The much larger weak Mordell--Weil and Selmer-group layers are deliberately not imported: callers may establish finite index of doubling by a curve-specific descent.

theorem WeierstrassCurve.Affine.den_duplication_eq {R : Type u_1} [CommRing R] {W' : WeierstrassCurve R} {x y : R} (h : W'.toAffine.Equation x y) : 4 * x ^ 3 + W'.b₂ * x ^ 2 + 2 * W'.b₄ * x + W'.b₆ = (2 * y + W'.a₁ * x + W'.a₃) ^ 2

theorem WeierstrassCurve.Affine.den_duplication_eq_zero_iff {R : Type u_1} [CommRing R] {W' : WeierstrassCurve R} [IsReduced R] {x y : R} (h : W'.toAffine.Equation x y) : 4 * x ^ 3 + W'.b₂ * x ^ 2 + 2 * W'.b₄ * x + W'.b₆ = 0 ↔ y = W'.toAffine.negY x y

theorem WeierstrassCurve.Affine.den_duplication_ne_zero_or_num_duplication_ne_zero {F : Type u_2} [Field F] {W : WeierstrassCurve F} {x y : F} (h : W.toAffine.Nonsingular x y) : 4 * x ^ 3 + W.b₂ * x ^ 2 + 2 * W.b₄ * x + W.b₆ ≠ 0 ∨ x ^ 4 - W.b₄ * x ^ 2 - 2 * W.b₆ * x - W.b₈ ≠ 0

theorem WeierstrassCurve.Affine.addX_self_of_Y_ne {F : Type u_2} [Field F] {W : WeierstrassCurve F} [DecidableEq F] {x y : F} (h : W.toAffine.Equation x y) (hn : y ≠ W.toAffine.negY x y) : W.toAffine.addX x x (W.toAffine.slope x x y y) = (x ^ 4 - W.b₄ * x ^ 2 - 2 * W.b₆ * x - W.b₈) / (4 * x ^ 3 + W.b₂ * x ^ 2 + 2 * W.b₄ * x + W.b₆)

theorem WeierstrassCurve.Affine.addX_of_X_ne {F : Type u_2} [Field F] {W : WeierstrassCurve F} [DecidableEq F] {xP yP xQ yQ : F} (hn : xP ≠ xQ) : W.toAffine.addX xP xQ (W.toAffine.slope xP xQ yP yQ) = ((yP - yQ) ^ 2 + W.a₁ * (yP - yQ) * (xP - xQ) - (W.a₂ + xP + xQ) * (xP - xQ) ^ 2) / (xP - xQ) ^ 2

theorem WeierstrassCurve.Affine.Point.xRep_add_self_of_Y_ne {F : Type u_2} [Field F] {W : WeierstrassCurve F} [DecidableEq F] {x y : F} (h : W.toAffine.Nonsingular x y) (hn : y ≠ W.toAffine.negY x y) : (some x y h + some x y h).xRep = ![(x ^ 4 - W.b₄ * x ^ 2 - 2 * W.b₆ * x - W.b₈) / (4 * x ^ 3 + W.b₂ * x ^ 2 + 2 * W.b₄ * x + W.b₆), 1]

theorem WeierstrassCurve.Affine.Point.xRep_add_self_of_Y_eq {F : Type u_2} [Field F] {W : WeierstrassCurve F} [DecidableEq F] {x y : F} (h : W.toAffine.Nonsingular x y) (hn : y = W.toAffine.negY x y) : (some x y h + some x y h).xRep = ![1, 0]

theorem WeierstrassCurve.Affine.Point.xRep_add_of_X_ne {F : Type u_2} [Field F] {W : WeierstrassCurve F} [DecidableEq F] {xP yP xQ yQ : F} (hP : W.toAffine.Nonsingular xP yP) (hQ : W.toAffine.Nonsingular xQ yQ) (hn : xP ≠ xQ) : (some xP yP hP + some xQ yQ hQ).xRep = ![((yP - yQ) ^ 2 + W.a₁ * (yP - yQ) * (xP - xQ) - (W.a₂ + xP + xQ) * (xP - xQ) ^ 2) / (xP - xQ) ^ 2, 1]

theorem WeierstrassCurve.Affine.Point.xRep_sub_of_X_ne {F : Type u_2} [Field F] {W : WeierstrassCurve F} [DecidableEq F] {xP yP xQ yQ : F} (hP : W.toAffine.Nonsingular xP yP) (hQ : W.toAffine.Nonsingular xQ yQ) (hn : xP ≠ xQ) : (some xP yP hP - some xQ yQ hQ).xRep = ![((yP + yQ + W.a₁ * xQ + W.a₃) ^ 2 + W.a₁ * (yP + yQ + W.a₁ * xQ + W.a₃) * (xP - xQ) - (W.a₂ + xP + xQ) * (xP - xQ) ^ 2) / (xP - xQ) ^ 2, 1]

theorem WeierstrassCurve.Affine.finite_preimage_xRep {F : Type u_2} [Field F] {W : WeierstrassCurve F} (x : F) : {P : W.toAffine.Point | P.xRep = ![x, 1]}.Finite

theorem WeierstrassCurve.Affine.finite_preimage_xRep0 {F : Type u_2} [Field F] {W : WeierstrassCurve F} (x : F) : {P : W.toAffine.Point | P.xRep 0 = x}.Finite

theorem WeierstrassCurve.Affine.Point.sym2x_eq {F : Type u_2} [Field F] {W : WeierstrassCurve F} (P Q : W.toAffine.Point) : P.sym2x Q = ![P.xRep 0 * Q.xRep 0, P.xRep 0 * Q.xRep 1 + P.xRep 1 * Q.xRep 0, P.xRep 1 * Q.xRep 1]

theorem WeierstrassCurve.Affine.Point.sym2x_add_sub_eq_addSubMap_sym2x {F : Type u_2} [Field F] {W : WeierstrassCurve F} [DecidableEq F] (P Q : W.toAffine.Point) : ∃ (t : F), t ≠ 0 ∧ t • (P + Q).sym2x (P - Q) = fun (i : Fin 3) => (MvPolynomial.eval (P.sym2x Q)) (W.addSubMap i)

noncomputable def WeierstrassCurve.Affine.Point.naiveHeight {F : Type u_2} [Field F] {W : WeierstrassCurve F} [Height.AdmissibleAbsValues F] (P : W.toAffine.Point) : ℝ

The logarithmic projective height of an affine point's x-coordinates.

Equations

• P.naiveHeight = Height.logHeight P.xRep

theorem WeierstrassCurve.Affine.Point.naiveHeight_eq_logHeight {F : Type u_2} [Field F] {W : WeierstrassCurve F} [Height.AdmissibleAbsValues F] (P : W.toAffine.Point) : P.naiveHeight = Height.logHeight P.xRep

theorem WeierstrassCurve.Affine.Point.naiveHeight_eq_logHeight₁ {F : Type u_2} [Field F] {W : WeierstrassCurve F} [Height.AdmissibleAbsValues F] {P : W.toAffine.Point} : P.naiveHeight = Height.logHeight₁ (P.xRep 0)

theorem WeierstrassCurve.Affine.abs_logHeight_sym2x_sub_le {F : Type u_2} [Field F] (W : WeierstrassCurve F) [Height.AdmissibleAbsValues F] : ∃ (C : ℝ), ∀ (P Q : W.toAffine.Point), |Height.logHeight (P.sym2x Q) - (P.naiveHeight + Q.naiveHeight)| ≤ C

theorem WeierstrassCurve.Affine.approx_parallelogram_law {F : Type u_2} [Field F] (W : WeierstrassCurve F) [Height.AdmissibleAbsValues F] [WeierstrassCurve.IsElliptic W.toAffine] [DecidableEq F] : ∃ (C : ℝ), ∀ (P Q : W.toAffine.Point), |(P + Q).naiveHeight + (P - Q).naiveHeight - 2 * (P.naiveHeight + Q.naiveHeight)| ≤ C

instance WeierstrassCurve.Affine.instNorthcottPointToAffineRealNaiveHeightOfLogHeight₁ {F : Type u_2} [Field F] (W : WeierstrassCurve F) [Height.AdmissibleAbsValues F] [Northcott Height.logHeight₁] : Northcott Point.naiveHeight

theorem WeierstrassCurve.Affine.fg_point_of_finiteIndex_two {F : Type u_2} [Field F] (W : WeierstrassCurve F) [Height.AdmissibleAbsValues F] [WeierstrassCurve.IsElliptic W.toAffine] [Northcott Height.logHeight₁] [DecidableEq F] (hindex : (nsmulAddMonoidHom 2).range.FiniteIndex) : AddGroup.FG W.toAffine.Point