The canonical (Néron–Tate) height #
The naïve height h is quadratic only up to a bounded error: approx_parallelogram_law gives a
constant C with |h(P + Q) + h(P - Q) - 2(h P + h Q)| ≤ C. Tate's observation is that averaging
that error away along the doubling map removes it. This file carries
out that construction and records the facts that pin the definition down: the limit exists, it
stays within a bounded distance of h, and it takes the expected values at 0 and under
negation, and it is honestly quadratic — it satisfies the parallelogram law exactly, which is
what the whole averaging was for.
canonicalHeight P = lim_{n → ∞} h(2ⁿ P) / 4ⁿ
The naïve height here is the height of the x-coordinate. We use the normalisation obtained by
averaging this height itself; the associated pairing and regulator use the same normalisation.
Main definitions #
WeierstrassCurve.Affine.Point.canonicalHeight: the limit above.WeierstrassCurve.Affine.canonicalHeightQuadratic: the canonical height as aℤ-quadratic map with real values, which is the form Mathlib's polarisation API consumes.WeierstrassCurve.Affine.neronTatePairing: the Néron–Tate pairing, the bilinear form associated with that quadratic map.
Main results #
WeierstrassCurve.Affine.Point.tendsto_naiveHeight_two_pow_nsmul_div_four_pow: the defining limit is attained, socanonicalHeightis the limit and not the junk valuelimUnderreturns when a sequence does not converge. Properties that genuinely need passage to the limit are proved by transporting a property ofhalong this; the values at0and under negation do not, and are proved termwise instead.WeierstrassCurve.Affine.Point.canonicalHeight_zeroandWeierstrassCurve.Affine.Point.canonicalHeight_neg: its values at the two points every consumer meets first, as@[simp]normal forms.WeierstrassCurve.Affine.Point.canonicalHeight_parallelogram_law: the canonical height satisfies the parallelogram law exactly, where the naïve height satisfies it only up to a bounded error. This is the point of the construction: it is the quadratic function the naïve height was approximating.WeierstrassCurve.Affine.Point.canonicalHeight_two_nsmul: the doubling normal formcanonicalHeight (2 • P) = 4 * canonicalHeight P, the parallelogram law atQ = P.WeierstrassCurve.Affine.Point.canonicalHeight_zsmulandWeierstrassCurve.Affine.Point.canonicalHeight_nsmul: the value atn • Pisn ^ 2times the value atP. This exhibits the canonical height as a quadratic form onW.Point; the general statement it specialises lives inTauCeti/LinearAlgebra/QuadraticForm/OfParallelogram.lean.WeierstrassCurve.Affine.Point.canonicalHeight_nonneg: it is non-negative, read off the defining sequence termwise.WeierstrassCurve.Affine.Point.canonicalHeight_eq_zero_iff_isOfFinAddOrder: it vanishes exactly on the torsion points. The two directions are also available separately, because they need different hypotheses:canonicalHeight_eq_zero_of_isOfFinAddOrderis quadraticity at a vanishing multiple and needs no finiteness, whileisOfFinAddOrder_of_canonicalHeight_eq_zeroassumes Northcott finiteness for the canonical height itself.WeierstrassCurve.Affine.Point.abs_canonicalHeight_sub_naiveHeight_le: the canonical height stays within a bounded distance of the naïve one, by a constant depending only on the curve. This is what makes the two interchangeable in finiteness arguments — in particular Northcott finiteness transfers to it, which theNorthcottinstance below makes formal.WeierstrassCurve.Affine.neronTatePairing_apply: the pairing is the polarisation — its value atP, Qis half ofcanonicalHeight (P + Q) - canonicalHeight P - canonicalHeight Q.WeierstrassCurve.Affine.neronTatePairing_self: it recovers the canonical height on the diagonal, so the pairing and the height determine each other.WeierstrassCurve.Affine.neronTatePairing_eq_zero_of_isOfFinAddOrder_leftandWeierstrassCurve.Affine.neronTatePairing_eq_zero_of_isOfFinAddOrder_right: it vanishes as soon as either argument is torsion, which is what lets it descend to the free quotientW.Point ⧸ torsionwhere the regulator is defined.WeierstrassCurve.Affine.neronTatePairing_commandWeierstrassCurve.Affine.neronTatePairing_flip: it is symmetric, pointwise and as an equality of bilinear maps.
Implementation notes #
The doubling bound |h(2P) - 4 h(P)| ≤ C is the approximate parallelogram law at Q = P, where
P - Q = 0 and h(0) = 0. Convergence needs only that specialisation, which is why it is
private; canonicalHeight_parallelogram_law needs the full two-point law, and takes it directly
from approx_parallelogram_law.
Convergence is cauchySeq_of_le_geometric at ratio 1/4: consecutive terms of
h(2ⁿ P) / 4ⁿ differ by
|h(2 · 2ⁿ P) - 4 h(2ⁿ P)| / 4ⁿ⁺¹ ≤ C / 4ⁿ⁺¹ = (C/4) · (1/4)ⁿ. The same estimate
feeds Mathlib's
dist_le_of_le_geometric_of_tendsto₀, which bounds the distance from the zeroth term — and the
zeroth term is h(P) — giving |canonicalHeight P - h(P)| ≤ (C / 4) / (1 - 1/4) = C / 3
with no further work.
The [DecidableEq F] hypothesis is not incidental: W.Point's AddCommGroup instance needs it,
since the addition formula case-splits on whether the two points share an x-coordinate. Without
it 2 ^ n • P does not elaborate.
References #
The canonical (Néron–Tate) height canonicalHeight P = lim h(2ⁿ P) / 4ⁿ,
normalised against the naïve height of the x-coordinate.
The limit exists whenever the curve is elliptic
(Point.tendsto_naiveHeight_two_pow_nsmul_div_four_pow); the definition itself needs no hypothesis
beyond those making 2 ^ n • P meaningful, so it is stated without one.
Equations
- P.canonicalHeight = Filter.atTop.limUnder fun (n : ℕ) => (2 ^ n • P).naiveHeight / 4 ^ n
Instances For
The defining limit is attained. canonicalHeight is limUnder, which returns a junk value
on a divergent sequence; this says the sequence converges, so the definition means what it says.
The point at infinity has canonical height zero: every term of the defining sequence is
h 0 / 4 ^ n = 0. This is termwise, so it needs no convergence and no ellipticity.
Negation preserves the canonical height, because it preserves the naïve height and commutes with doubling, so the two defining sequences agree termwise — again with no convergence or ellipticity needed.
The canonical height differs from the naïve height by a bounded amount, the bound
depending only on the curve. This is the normalisation described in the module docstring;
Northcott finiteness for h transfers to the canonical height through this.
The canonical height satisfies the parallelogram law exactly.
The naïve height satisfies it only up to a bounded error (approx_parallelogram_law); dividing
that error by 4ⁿ and letting n → ∞ removes it. This is what the construction is for: the
canonical height is the quadratic function that h was approximating.
Doubling scales the canonical height by four. The parallelogram law at Q = P, where
P - Q = 0 contributes nothing.
The canonical height is non-negative. This is what makes it a candidate for the
positive-definite form behind the Néron–Tate pairing and the regulator, and what lets
canonicalHeight P = 0 be a meaningful characterisation of torsion rather than one inequality
among two.
The canonical height is quadratic in the point: it takes n • P to n ^ 2 times its
value at P, for an integer n.
The canonical height is quadratic in the point, for a natural multiple.
A torsion point has canonical height zero. Unlike the converse this needs no Northcott hypothesis, so it holds over every field carrying admissible absolute values.
Northcott finiteness transfers from the naïve height to the canonical one. This is what
lets the results below assume Northcott for the canonical height itself while callers supply only
the naïve height — or, through MordellWeil/NaiveHeight.lean, only the field height.
A point of canonical height zero is torsion. The hypothesis is Northcott for the
canonical height, the class this API takes finiteness from; the instance above supplies it from
the naïve height and MordellWeil/NaiveHeight.lean from the field height, so a caller carrying
either of those needs nothing extra.
The canonical height vanishes exactly on the torsion points, identifying the kernel of
the canonical height with the torsion subgroup. This is one input to positive definiteness on the
free part, and so to the regulator; the others — polarising it, and finite generation of W.Point
— are elsewhere, and neither is supplied here.
The canonical height as a ℤ-quadratic map with values in ℝ, which is what makes
Mathlib's polarisation API available to it.
Equations
Instances For
The quadratic map is the canonical height.
The quadratic map is the canonical height, as functions.
The Néron–Tate pairing ⟨P, Q⟩, the bilinear form associated with the canonical height.
It is Mathlib's QuadraticMap.associated', the halved polar form.
Instances For
The Néron–Tate pairing is the polarisation of the canonical height: its value at P, Q
is half of canonicalHeight (P + Q) - canonicalHeight P - canonicalHeight Q.
The pairing recovers the canonical height on the diagonal.
The pairing kills torsion in its first argument. Together with symmetry this is what lets
the pairing descend to the free quotient W.Point ⧸ torsion, where the regulator lives.
The pairing is symmetric: ⟨P, Q⟩ = ⟨Q, P⟩.
The pairing kills torsion in its second argument.
The pairing is reflexive, being symmetric. Reflexivity is what permits a symmetric bilinear descent to a quotient.
The pairing is symmetric, as an equality of bilinear maps.