The regulator of an elliptic curve #

The regulator is the absolute value of the determinant of the Néron-Tate pairing's Gram matrix on a basis of the points modulo torsion. It does not depend on the basis chosen: a change of basis transforms the Gram matrix by congruence, G' = Mᵀ G M, along the integer change-of-basis matrix M. The two bases need not be indexed by the same type, in which case M is rectangular and has no determinant; the absolute determinant is invariant all the same, because the index types of two bases of the same module are equivalent.

Main definitions #

WeierstrassCurve.Affine.regulator: the regulator of a curve whose points modulo torsion are finitely generated as a ℤ-module.

Main results #

WeierstrassCurve.Affine.neronTateGramMatrix_basis_change: a change of basis acts on the Gram matrix by congruence.
WeierstrassCurve.Affine.abs_det_neronTateGramMatrix_basis_change: the absolute determinant is independent of the basis, including of its index type.
WeierstrassCurve.Affine.regulator_eq_abs_det_neronTateGramMatrix: the regulator is computed by any basis whatsoever.
WeierstrassCurve.Affine.regulator_eq_one_of_finrank_eq_zero: the rank-zero convention.
WeierstrassCurve.Affine.regulator_nonneg: the regulator is non-negative.

References #

J. Silverman, The Arithmetic of Elliptic Curves, VIII.9, where the canonical height and its associated pairing are constructed; the regulator is the determinant of that pairing's Gram matrix on a basis of the free quotient.

source

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

W.neronTateGramMatrix b' = ((b.toMatrix ⇑b').map Int.cast).transpose * W.neronTateGramMatrix b * (b.toMatrix ⇑b').map Int.cast

A change of basis acts on the Gram matrix of the Néron-Tate pairing by congruence, along the integer change-of-basis matrix. The two bases need not share an index type: the change-of-basis matrix is then rectangular, and the congruence still typechecks.

source

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

|(W.neronTateGramMatrix b').det| = |(W.neronTateGramMatrix b).det|

The absolute determinant of the Gram matrix does not depend on the basis, nor on its index type.

source

noncomputable def WeierstrassCurve.Affine.regulator {F : Type u_1} [Field F] (W : Affine F) [Height.AdmissibleAbsValues F] [DecidableEq F] [WeierstrassCurve.IsElliptic (toAffine W)] [Module.Finite ℤ W.PointModTorsion] :

ℝ

The regulator of an elliptic curve whose points modulo torsion are finitely generated as a ℤ-module: the absolute determinant of the Gram matrix of the Néron-Tate pairing on any basis of that quotient. For a curve of rank zero this is the empty determinant, namely 1.

Equations