The points modulo torsion, and the Néron-Tate pairing on them

The Néron-Tate pairing vanishes as soon as either argument is torsion, so it descends to the quotient of the points by their torsion submodule, unconditionally. Under [Northcott (Point.canonicalHeight (W := W))] — the hypothesis that makes height zero force torsion — the descended pairing is moreover positive definite. That quotient is where the regulator is defined.

Main definitions

• WeierstrassCurve.Affine.PointModTorsion: the points modulo torsion. Neither its freeness nor its rank is restated here, both being Mathlib's: under [AddGroup.FG W.Point] the quotient is free of finite rank by Module.free_of_finite_type_torsion_free', and its rank is Module.finrank ℤ W.Point by finrank_quotient_eq_of_le_torsion at le_rfl. The definition itself assumes neither, so the name says only what the quotient is.
• WeierstrassCurve.Affine.neronTatePairingModTorsion: the Néron-Tate pairing on that quotient.
• WeierstrassCurve.Affine.neronTateGramMatrix: its matrix in a basis, whose determinant is the regulator.

Main results

• WeierstrassCurve.Affine.torsion_le_ker_neronTatePairing: the pairing kills the torsion submodule, which is what the descent consumes.
• WeierstrassCurve.Affine.neronTatePairingModTorsion_mk: the descended pairing agrees with the original on representatives.
• WeierstrassCurve.Affine.neronTatePairingModTorsion_self_eq_zero_iff: the descended pairing is positive definite, given the Northcott hypothesis. This is what dividing by the torsion buys; on W.Point itself the pairing is only semidefinite.
• WeierstrassCurve.Affine.isSymm_neronTateGramMatrix: the Gram matrix is symmetric. The regulator is the determinant of this matrix in a basis of the quotient, and is defined separately.

@[reducible, inline]

abbrev WeierstrassCurve.Affine.PointModTorsion {F : Type u_1} [Field F] (W : Affine F) [DecidableEq F] : Type u_1

The points modulo torsion, the Mordell-Weil group with its torsion divided out.

Equations

• W.PointModTorsion = (W.Point ⧸ Submodule.torsion ℤ W.Point)

theorem WeierstrassCurve.Affine.torsion_le_ker_neronTatePairing {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] : Submodule.torsion ℤ W.Point ≤ LinearMap.ker W.neronTatePairing

The pairing vanishes on the torsion submodule, which is what the descent consumes.

noncomputable def WeierstrassCurve.Affine.neronTatePairingModTorsion {F : Type u_1} [Field F] (W : Affine F) [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] : LinearMap.BilinMap ℤ W.PointModTorsion ℝ

The Néron-Tate pairing on the points modulo torsion.

Equations

• W.neronTatePairingModTorsion = LinearMap.IsRefl.liftQ₂ W.neronTatePairing (Submodule.torsion ℤ W.Point) ⋯ ⋯

@[simp]

theorem WeierstrassCurve.Affine.neronTatePairingModTorsion_mk {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] (P Q : W.Point) : (W.neronTatePairingModTorsion (Submodule.Quotient.mk P)) (Submodule.Quotient.mk Q) = (W.neronTatePairing P) Q

The descended pairing agrees with the pairing on representatives.

theorem WeierstrassCurve.Affine.neronTatePairingModTorsion_comm {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] (x y : W.PointModTorsion) : (W.neronTatePairingModTorsion x) y = (W.neronTatePairingModTorsion y) x

The descended pairing is symmetric.

@[simp]

theorem WeierstrassCurve.Affine.neronTatePairingModTorsion_flip {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] : LinearMap.flip W.neronTatePairingModTorsion = W.neronTatePairingModTorsion

The descended pairing is symmetric, as an equality of bilinear maps.

Positive definiteness

theorem WeierstrassCurve.Affine.neronTatePairingModTorsion_self_nonneg {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] (x : W.PointModTorsion) : 0 ≤ (W.neronTatePairingModTorsion x) x

The descended pairing is non-negative on the diagonal, the canonical height being so.

@[simp]

theorem WeierstrassCurve.Affine.neronTatePairingModTorsion_self_eq_zero_iff {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] [Northcott Point.canonicalHeight] (x : W.PointModTorsion) : (W.neronTatePairingModTorsion x) x = 0 ↔ x = 0

The descended pairing is positive definite: its diagonal vanishes only at zero. This is what dividing by the torsion buys, the canonical height vanishing exactly on the torsion. The Northcott hypothesis is the one that makes height zero force torsion, and it is what Point.canonicalHeight_eq_zero_iff_isOfFinAddOrder consumes.

The Gram matrix

noncomputable def WeierstrassCurve.Affine.neronTateGramMatrix {F : Type u_1} [Field F] (W : Affine F) [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] {ι : Type u_2} (b : Module.Basis ι ℤ W.PointModTorsion) : Matrix ι ι ℝ

The Gram matrix of the Néron-Tate pairing in a basis of the quotient.

Equations

• W.neronTateGramMatrix b = (LinearMap.toMatrix₂Aux ℤ ⇑b ⇑b) W.neronTatePairingModTorsion

@[simp]

theorem WeierstrassCurve.Affine.neronTateGramMatrix_apply {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] {ι : Type u_2} (b : Module.Basis ι ℤ W.PointModTorsion) (i j : ι) : W.neronTateGramMatrix b i j = (W.neronTatePairingModTorsion (b i)) (b j)

Each Gram-matrix entry is the descended pairing of the corresponding basis vectors.

@[simp]

theorem WeierstrassCurve.Affine.neronTateGramMatrix_reindex {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] {ι : Type u_2} {ι' : Type u_3} (b : Module.Basis ι ℤ W.PointModTorsion) (σ : ι ≃ ι') : W.neronTateGramMatrix (b.reindex σ) = (W.neronTateGramMatrix b).submatrix ⇑σ.symm ⇑σ.symm

Reindexing the basis permutes the Gram matrix.

theorem WeierstrassCurve.Affine.isSymm_neronTateGramMatrix {F : Type u_1} [Field F] {W : Affine F} [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] {ι : Type u_2} (b : Module.Basis ι ℤ W.PointModTorsion) : (W.neronTateGramMatrix b).IsSymm

The Gram matrix is symmetric, the pairing being so.