feat(NumberTheory/Height/EllipticCurve): new file

[MichaelStollBayreuth]

This PR defines the "addition-and-subtraction map" on x-coordinates of pairs of points on elliptic curves and proves an inequality for the logarithmic height of the image.

In a later PR, we will show that the map thus defined indeed comes from addition and subtraction on an elliptic curve.

---

[github-actions]

PR summary 68e18bf8ed

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap (new file)	1303
Mathlib.NumberTheory.Height.EllipticCurve (new file)	1792

---

Declarations diff

+ abs_logHeight_addSubMap_sub_two_mul_logHeight_le
+ addSubMap
+ addSubMapCoeff
+ addSubMapCoeff_condition
+ addSubMap_ne_zero
+ isHomogeneous_addSubMap
+ isHomogenous_addSubMapCoeff

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Multramate]

I'm going to have a look at this later in the week, but I would argue that it should be in the EllipticCurve(/NumberField?) folder instead. Although I note it's still field independent at this point so I don't know...

[MichaelStollBayreuth]

The last bit is a height inequality (but it is valid over any field with a height, so not number field specific), so it needs heights; this is why I have put it under NumberTheory.Height.
The material prior to that and also the part (to come later) that shows that the map I define is the correct one could also go somewhere under AlgebraicGeometry.EllipticCurve.Affine; maybe a new file?

[MichaelStollBayreuth]

Moved the material to two files under AlgebraicGeometry.EllipticCurve.Affine:

• AddSubMap: for the height-independent material on the addition-and-subtraction map on x-coordinates
• NaiveHeight: for the definition of the naïve height and the material based on heights leading up to the approximate parallelogram law

[MichaelStollBayreuth]

However, I then get

Warning: warning: Mathlib/AlgebraicGeometry/EllipticCurve/Affine/NaiveHeight.lean:11:0: Modules starting with Mathlib.AlgebraicGeometry are not allowed to import modules starting with Mathlib.Analysis. This module depends on Mathlib.Analysis.Normed.Group.Seminorm

on the NaiveHeight file.

[MichaelStollBayreuth]

So I will move that file back to under NumberTheory.Height for the time being.

[MichaelStollBayreuth]

Now

Warning: warning: Mathlib/NumberTheory/Height/EllipticCurve.lean:11:0: Modules starting with Mathlib.NumberTheory are not allowed to import modules starting with Mathlib.AlgebraicGeometry. This module depends on Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

🤷

[riccardobrasca]

I think it's fine to add an exception here.

[MichaelStollBayreuth]

I think it's fine to add an exception here.

For which of the two possible placements of the file? (Allow AlgebraicGeometry... to import Analysis, or allow NumberTheory.Height.... to import AlgebraicGeometry?)

[riccardobrasca]

I think it's fine to add an exception here.

For which of the two possible placements of the file? (Allow AlgebraicGeometry... to import Analysis, or allow NumberTheory.Height.... to import AlgebraicGeometry?)

I would put the file in NumberTheory, but do whatever you prefer. This warning are mostly about basic stuff.

[Multramate]

I would think it's a "height theory for elliptic curves" rather than an "elliptic curve theory for heights" eo I would put them in the elliptic curve folder. I have been thinking of moving everything into NumberTheory since it doesn't use anything in AlgebraicGeometry (except for Affine.Scheme), but if we were to make ArithmeticGeometry...