Elementary properties of the naïve height on an elliptic curve

Mathlib defines the naïve height Point.naiveHeight P = logHeight P.xRep of an affine point of a Weierstrass curve, proves the approximate parallelogram law for it and deduces Northcott finiteness. This file adds the three pointwise facts that the canonical height needs and that Mathlib does not state: non-negativity, the value at the point at infinity, and invariance under negation.

Main results

• WeierstrassCurve.Affine.Point.naiveHeight_nonneg : the naïve height is non-negative.
• WeierstrassCurve.Affine.Point.naiveHeight_zero : the point at infinity has height zero.
• WeierstrassCurve.Affine.Point.naiveHeight_neg : negation preserves the naïve height.

References

• M. Stoll, EllipticCurves, commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, EllipticCurves/MordellWeil.lean, Apache-2.0.

theorem WeierstrassCurve.Affine.Point.naiveHeight_nonneg {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] {W : Affine F} (P : W.Point) : 0 ≤ P.naiveHeight

The naïve height is non-negative, being a logarithmic height.

@[simp]

theorem WeierstrassCurve.Affine.Point.naiveHeight_zero {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] {W : Affine F} : naiveHeight 0 = 0

The point at infinity has height zero: its representative is ![1, 0].

@[simp]

theorem WeierstrassCurve.Affine.Point.naiveHeight_neg {F : Type u_1} [Field F] [Height.AdmissibleAbsValues F] {W : Affine F} (P : W.Point) : (-P).naiveHeight = P.naiveHeight

Negation preserves the naïve height, since P and -P share an x-coordinate.