Heights

Stream: PR reviews

[Michael Stoll]

It may make sense to move the discussion on the PRs introducing heights and their properties from #maths > thoughts on elliptic curves @ 💬 to a dedicated thread in this channel.

#34330 is the third PR; its main part proves bounds for the height of a sum (of two or arbitrarily many field elements). It also adds positivity extensions for the various kinds of heights and adds a few API lemmas for products on Multisets and on finprods. One of these leads to a significant import increase in Mathlib/Algebra/BigOperators/Finprod.lean (it is not a public import, however). The alternative would be to put finprod_le_finprod into a new file (#find_home! didn't find a good place for it). This can be discussed in the PR comments.

[Johan Commelin]

I finally had some time to look at this.

Could you split the positivity extension into a separate PR?

And maybe all the API lemmas into another one? (Those parts are probably a quick merge.)

[Michael Stoll]

@Johan Commelin Done. #34533 contains the API lemmas.

[Michael Stoll]

... and #34534 the positivity extensions. I hope I have set up the dependency correctly.

[Johan Commelin]

Dependency setup looks good. Only think I did was put those references below the --- fold. So that they don't end up in the final commit message on master.

[Michael Stoll]

@Anne Baanen Could you have a quick look at #34534 again?

[Michael Stoll]

#34330 can now be looked at again; the dependencies have been merged.

[Michael Stoll]

#34776 just changes the name of "NumberTheory.Height.Instances" to "NumberTheory.Height.NumberField". So far, this file contains the docs#Height.AdmissibleAbsValues instance for number fields and already some number field specific results on heights. As I anticipate adding more number field specific results in the future, I think it makes sense to have a dedicated file for that. (After the move, the module docstring needs some updating, and the TODOs should be moved to the Basic file. I will do this in a follow-up PR, once this is merged.)

[Michael Stoll]

#34780 adds a new file "NumberTheory.Height.Projectivization" that contains the definition of multiplicative and logarithmic height of points in projective space, plus basic properties and positivity extensions analogous to those for heights of field elements and tuples.

I'm putting this into a separate file since I expect the "Basic" file to grow quite a bit over time and I also expect that quite some material will be added on the projective side (the goal would be to prove Weil's "Height Machine" eventually).

[Michael Stoll]

@Johan Commelin Is it OK if I assign you to #34330? You already had looked at it.

[Michael Stoll]

@Johan Commelin I've made the assignment now. Feel free to unassign yourself again.

[Johan Commelin]

Sorry, had very little review time this week. But I'll look at this next week. Thanks for the ping.

[Michael Stoll]

@Johan Commelin Can I ping you again on #34330 (and possibly also #34780)?
I have some more PRs in the pipeline and would like to have this in first.

[Michael Stoll]

The PRs mentioned in the next few posts are independent of the two mentioned above.

#35258 is one of a few PRs that adds API lemmas, in this case one lemma (now two lemmas) for docs#Finsupp.

[Michael Stoll]

#35259 adds two API lemmas for multivariate polynomials, an API lemma for docs#Polynomial.homogenize, and a definition (homogenize a polynomial map on the affine map to a polynomial map on the projective line) with some API for it.

[Michael Stoll]

#35260 adds convenience API lemmas for ciSup/ciInf-related statements in the case when the indexing type is finite (and so the boundedness condition is automatic). It then uses them to golf a few proofs.

[Johan Commelin]

Unfortunately, I'm short on time. Hopefully others can step in.

[Riccardo Brasca]

I will have a look later this week.

[Antoine Chambert-Loir]

I had made one suggestions on one of the files. I had a look at all the other, and found nothing interesting to add. This looks good to me.

[Michael Stoll]

@Antoine Chambert-Loir It may perhaps help to leave an approving review.

[Michael Stoll]

#35407 does some minor stuff in NumberTheory.Height.Basic (fix names, add to_fun, add two API lemmas for docs#Height.logHeight parallel to existing ones for docs#Height.mulHeight).

[Michael Stoll]

#35408 adds more interesting material:

• {mul|log}Height_comp_le: the height of x ∘ f is bounded by the height of x
• {mul|log}Height_fun_mul_eq: the height of the "multiplication table" fun (i, j) ↦ x i * y j is the {product|sum} of the heights of x and of y
• {mul|log}Height_fun_prod_eq: the analogous result for products with arbitrarily many factors