Heights on rational elliptic curves

Stream: maths

[David Ang]

I have defined a naive height function on an elliptic curve over the rationals based on Silverman's book, and proved that it satisfies the three descent lemmas in a ~1000-line file in the mordell_weil branch. Since my group law is not completely ready (API issues, missing associativity), and ideally we'd like to do height functions for elliptic curves over an arbitrary number field, this is likely never going to be PR'ed.

If anyone's interested, could you provide me with some feedback on this? Specifically, I was wondering if there are some shortcuts I could have taken to significantly shorten some of the proofs, since I plan to replicate parts of this for the general case to be done next.

Furthermore, it seems that to do the same over number fields would require some facts about local fields, at least in the references I am aware of. We do not have much API for local fields as of yet, so does anyone know of a way to get around this?