Defining n-division polynomials

Stream: maths

[Marc Masdeu]

Hi all,

I'm having a go at proving in Lean something that can't be found in the literature (as far as I'm aware), namely a purely algebraic proof of the validity of the formulas for the multiplication-by-n isogeny on elliptic curves. This involves the infamous n-division polynomials, which I am trying to define in Lean. The recurrence has 5 basic cases (0,1,2,3,4) and then two recurrent formulas, depending on the parity of n. I haven't been able to make it work so far, here is my try:

import tactic
import data.polynomial.basic
open polynomial

noncomputable theory
--variables {R : Type} [comm_ring R]
variables {A B : ℤ}
def x := (monomial 1 (1 : ℤ))

--set_option trace.eqn_compiler.elim_match true
noncomputable def psi : ℕ → (polynomial ℤ)
| 0 := 0
| 1 := 1
| 2 := 1
| 3 := 3*x^4 + 6*A*x^2 + 12*B*x - A^2*x
| 4 := 2*(x^6 + 5*A*x^4+20*B*x^3-5*A^2*x^2-4*A*B*x-A^3-8*B^2)
| (2*n+5) :=
  have n+4 < 2*n+5, by linarith,
  have n+3 < 2*n+5, by linarith,
  have n+2 < 2*n+5, by linarith,
  have n+1 < 2*n+5, by linarith,
  (psi (n+4)) * (psi (n+2))^3 - (psi (n+1) * (psi (n+3))^3)
| (2*n+6) :=
  have n+5 < 2*n+6, by linarith,
  have n+4 < 2*n+6, by linarith,
  have n+3 < 2*n+6, by linarith,
  have n+2 < 2*n+6, by linarith,
  (psi (n+3)) * ((psi (n+5))*
      (psi (n+2))^2 - (psi (n+1)) * (psi (n+4))^2) / (4*(x^3+A*x+B)),

From reading https://leanprover-community.github.io/extras/well_founded_recursion.html I gathered that I needed to supply the proofs of the fact that the recurrence is well-founded, but they would all be easy, I could even figure out how to produce a term proof if linarith was forbidden.

Also, I'd like A and B to be allowed to live in any commutative ring, but then it gives me even more errors because apparently A*x is not a polynomial in R when A is in R (but that's for a different thread I guess).

Any hints would be appreciated :-).

PS: feel free to move this to "new members", I'm not always sure of the distinction between streams.

[Kevin Buzzard]

I think you're no longer new :-) Just to be clear -- this is the y^2=x^3+Ax+B model, right?

[Kevin Buzzard]

The equation compiler isn't going to be able to split between even and odd cases I don't think, because even v odd is not something which comes directly from the recursive definition of the naturals. I would just be tempted to use "strong recursion" here.

[Marc Masdeu]

(what if not new but have a newbie question?). This is the y^2=x^3+Ax+B model, but if that worked then it shouldn't be too hard to adapt the proof to the general Weierstrass model.

[Marc Masdeu]

Oh, so you say that 2n vs 2n+1 (or what I write) does confuse lean? Maybe there's an easier way just defining phi_odd and phi_even, then? It wouldn't be as elegant, but I just want to type a proof...

[Johan Commelin]

Marc Masdeu said:

Also, I'd like A and B to be allowed to live in any commutative ring, but then it gives me even more errors because apparently A*x is not a polynomial in R when A is in R (but that's for a different thread I guess).

Use C A * X or A \bullet X. Here C is polynomial.C is the ring morphism from R to polynomial R.

(I think this thread perfectly fits the #maths stream!)

[Johan Commelin]

@Marc Masdeu I think would use if .. then .. else in the n + 5 branch

[Johan Commelin]

And nat-division, which is truncating, so 5/2 = 2, 6/2 = 3, and 7/2 = 3, etc...

[Johan Commelin]

The other option is the strong recursion that Kevin mentioned

[Kevin Buzzard]

Aah very nice, so you don't have to extract the k from "exists k, n=2k or n=2k+1"

[Kevin Buzzard]

I was going to suggest matching on the pos_num :-) but integer division is a much more sensible approach

[Kevin Buzzard]

So in conclusion do the final match on n+5 and use if then else on even (n+5) (or probably even n is more sensible) and try your have technique. And for the polynomials I would be tempted to fix a ring and just use polynomial.X directly (open polynomial first) and then use C or bub

[Marc Masdeu]

Thanks for the suggestions, I'll try and see.

[Marc Masdeu]

Seems that I've made a bit of progress:

import tactic
import data.polynomial.basic
open polynomial

noncomputable theory
variables {R : Type} [comm_ring R]
variables {A B : R}
def x := (monomial 1 (1 : R))

--set_option trace.eqn_compiler.elim_match true
noncomputable def psi : ℕ → (polynomial R)
| 0 := 0
| 1 := 1
| 2 := 1
| 3 := 3*x^4 + 6*A•x^2 + 12*B•x - A^2•x
| 4 := 2*(x^6 + 5*A•x^4+20*B•x^3-5*A^2•x^2-(4*A*B)•x-A^3•x^0-8*B^2•x^0)
| (n+5) :=
  have n/2+1 < n+5, by sorry,
  have n/2+2 < n+5, by sorry,
  have n/2+3 < n+5, by sorry,
  have n/2+4 < n+5, by sorry,
  have n/2+5 < n+5, by sorry,
  if even n then (psi (n/2+3)) * ((psi (n/2+5))*
      (psi (n/2+2))^2 - (psi (n/2+1)) * (psi (n/2+4))^2) --/ (4*(x^3+A•x+B•x^0))
      else
  (psi (n/2+4)) * (psi (n/2+2))^3 - (psi (n/2+1) * (psi (n/2+3))^3)

but Lean complains about decidable (even n). Also I'll have trouble dividing by a polynomial, I need to familiarize myself with that part of mathlib, but I'd have assumed that there is a has_div giving out junk when the numerator is not a multiple of the denominator, as usual.

[Johan Commelin]

I'm surprised that it complains about decidable (even n). But I guess you can replace it with n % 2 = 0 or open_locale classical.

[Johan Commelin]

n % 2 = 0 might be a bit easier, because it allows you to use rfl in a bit more places.

[Johan Commelin]

Of course the other option is to write an instance for decidable (even n). I didn't find it in mathlib with a quick search.

[Johan Commelin]

Anyway, the first thing after this definition is probably simp-lemmas for 0, 1, 2, 3, 4, even n, and odd n. Maybe also for 2n + 5 and 2n + 6.

[Kevin Buzzard]

And also I would be tempted to use polynomial.X rather than your x because there will be a bunch of lemmas about how X evaluates but you'll be constantly unfolding your x in order to make progress

[Kevin Buzzard]

import tactic
import data.nat.parity

example (n : ℕ) : decidable (even n) := infer_instance

It is there, you just need the right import perhaps?

[Marc Masdeu]

For what is worth, I post the definition I settled on.

import tactic
import data.polynomial.basic
import data.polynomial.div
import data.nat.parity
open polynomial
open nat

noncomputable theory
open_locale classical

lemma nhalves {n m r : ℕ} :  n / 2 + m < n + m + r + 1 :=
begin
  have twopos : 0 < 2, by linarith,
  have : n < 2*(n+1), by linarith,
  suffices : n / 2  < n+1,
  by linarith,
  exact nat.div_lt_of_lt_mul this,
end

lemma nhalves' {n m r : ℕ} : (n+1)/2 + m < n + m + r + 1:=
begin
  suffices : (n+1)/2 + m < n + m + 1, by linarith,
  suffices : (n+1)/2 < n + 1, by linarith,
  exact nat.div_lt_self' n 0,
end

/--
Define the "depleted" psi polynomials. They are Ψ as in Wikipedia,
but for even n we remove a factor of 2*y, thus making them one-variable.
-/
noncomputable def psi {R : Type*} [comm_ring R] (A B : R) : ℕ → (polynomial R)
| 0 := (0 : polynomial R)
| 1 := (1 : polynomial R)
| 2 := (1 : polynomial R)
| 3 := 3*X^4 + 6*A•X^2 + 12*B•X - A^2•1
| 4 := 2*(X^6 + 5*A•X^4+20*B•X^3-5*A^2•X^2-(4*A*B)•X-A^3•1-8*B^2•1)
| (n+5) :=
  have n/2+4 < n+4+0+1 := nhalves,
  have n/2+3 < n+3+1+1 := nhalves,
  have n/2+2 < n+2+2+1 := nhalves,
  have n/2+1 < n+1+3+1 := nhalves,
  have (n+1)/2 < n+0+4+1 := @nhalves' _ 0 _,
  have (n+1)/2+1 < n+1+3+1 := nhalves',
  have (n+1)/2+2 < n+2+2+1 := nhalves',
  have (n+1)/2+3 < n+3+1+1 := nhalves',
  have (n+1)/2+4 < n+4+0+1 := nhalves',
  if even n then
    if even (n / 2) then
      16*(X^3+A•X+B•1)^2 * psi (n/2+4) * (psi (n/2+2))^3 - psi (n/2+1) * (psi (n/2+3))^3
    else
      psi (n/2+4) * (psi (n/2+2))^3 - 16*(X^3+A•X+B•1)^2 * psi (n/2+1) * (psi (n/2+3))^3
  else
      (psi ((n+1)/2+2)) * ((psi ((n+1)/2+4)) * (psi ((n+1)/2+1))^2 -
        psi ((n+1)/2) * (psi ((n+1)/2+3))^2)

I have been able to prove the lemma, for example, with quite a bit of work. But it would be useful to avoid having to write A B so many times in such statements. For my application, I'd like to "fix" A B throughout a namespace, and define something like mypsi (or better, Ψ) like Ψ : ℕ → polynomial R := λ n, psi A B n, but I don't know how to do it, really.

lemma psi_two_times {A B : R} {n : ℕ}  (h : 2 ≤ n) :
 psi A B (2*n) = (psi A B n) * (psi A B (n+2) * (psi A B (n-1))^2 -
  psi A B (n-2) * (psi A B (n+1))^2 ) := sorry

[Johan Commelin]

@Marc Masdeu One possibility would be to use notation for this:

local notation `mypsi` := `psi A B`

That way you don't have to write the A and B everywhere in your code. But they will still be visible in the goal window.

[Mario Carneiro]

you mean local notation `mypsi` := psi A B

[Damiano Testa]

Hi Marc!

Not at all related to the A B stuff, but the initial lemmas can be proved as follows. I was actually surprised that lemma nat.half_le_self is not already in mathlib (and maybe it is?):

lemma nat.half_le_self (n : ℕ) : (n + 1) / 2 ≤ n :=
begin
  cases n,
  { exact rfl.le },
  { exact nat.div_le_of_le_mul (((add_le_add_iff_left _).mpr ((1 : ℕ).le_add_left n)).trans
      (two_mul _).symm.le) }
end

lemma nhalves {n m r : ℕ} :  n / 2 + m < n + m + r + 1 :=
(((add_le_add_iff_right _).mpr (n.div_le_self 2)).trans (le.intro rfl)).trans_lt (lt_add_one _)

lemma nhalves' {n m r : ℕ} : (n+1)/2 + m < n + m + r + 1:=
(((add_le_add_iff_right _).mpr n.half_le_self).trans (le.intro rfl)).trans_lt (lt_add_one _)

[Yakov Pechersky]

Check if there is such a statement about div2

[Damiano Testa]

I thought that I checked: besides library_search, I also tried with the autocomplete, but all my guesses failed. I did find the one with n / 2 ≤ n, though...

[Damiano Testa]

There is a possibly promising lemma, but I am not sure what it says:

@[simp] lemma div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) :=
by unfold bodd div2 bodd_div2; cases bodd_div2 n; cases fst; refl

[Damiano Testa]

Also, I am at the same time proud and ashamed of having guessed that (0 + 1) / 2 ≤ 0 was

• true,
• proved by exact rfl.le.

[Damiano Testa]

Johan, I wish I could add emoji reactions to your emoji reactions! :lol:

[Damiano Testa]

In case you find this helpful, I made a PR with the lemma (n+1) / 2 ≤ n.
#6863

[Damiano Testa]

Marc, lemma nat.succ_half_le_self did not survive the review process. However, with the latest version of mathlib, what's below is also a proof.

lemma nat.succ_half_le_self (n : ℕ) : (n + 1) / 2 ≤ n :=
(div_le_iff_le_mul_add_pred zero_lt_two).mpr ((add_le_add_iff_right _).mpr
  (le_mul_of_one_le_of_le one_le_two rfl.le))

If you do not care about lines longer than 100 chars, it even fits on a single line. :upside_down:

[Bhavik Mehta]

Every proof is a one line proof if you start far enough to the left :upside_down:

[Johan Commelin]

By induction every proof fits in the margin?

[David Ang]

Sorry for bringing up such an old post, but I'm very much stuck on a tiny part on what @Marc Masdeu was trying to prove a few years ago. As Marc said, I don't believe there is a complete proof in the literature for the formula for multiplication-by-n on an elliptic curve, and trying to fill the gaps has been rather annoying.

First of all one of the division polynomials in Silverman is defined incorrectly, and most online references point to Silverman when they refer to a "purely algebraic proof" that works over arbitrary characteristic. There is a set of MIT lecture notes that does this for characteristic > 3, which I believe can be generalised to characteristic 2/3, but I think their argument is incomplete: their inductive step isn't trivial for when $\psi_n(x, y) = 0$ since e.g. you have to prove that $-\psi_{n + 1}(x, y)\psi_{n - 1}(x, y)$ is a square in these cases, and I don't know how to do this. I think the most promising way to do this is to first show that $\psi_n$ and $\phi_n^2$ are relatively prime polynomials whenever the discriminant is a unit (I can show this for $n = 2$), but I don't know how to do this without first assuming the formula for multiplication-by-n, which is what I'm trying to prove. Any ideas how to do this?

In terms of Lean code, we already have Jacobian coordinates and a few PRs on the Jacobian group law and degrees of division polynomials. Once I have this tiny bit settled it should hopefully be smooth sailing all the way till the end.

[Antoine Chambert-Loir]

What happens when you write (n+1)p + (n-1)p=2(np)?

[Riccardo Brasca]

Note that #10814 is labelled "awaiting author".

[Riccardo Brasca]

Since you didn't get a good answer on stackexchange, have you considered asking the same question on mathoverflow?

[Antoine Chambert-Loir]

Schoof refers to Lang, Elliptic curves — Diophantine analysis.

[David Ang]

Antoine Chambert-Loir said:

What happens when you write (n+1)p + (n-1)p=2(np)?

Can you elaborate? I'm not sure how this is going to help. Here is my thought process: if we decompose $2nP$ as $(n + 1)P + (n - 1)P$ we'd have to show $(\phi_{n + 1}(x) : \omega_{n + 1}(x, y) : \psi_{n + 1}(x, y)) + (\phi_{n - 1}(x) : \omega_{n - 1}(x, y) : \psi_{n - 1}(x, y)) = (\phi_{2n}(x) : \omega_{2n}(x, y) : \psi_{2n}(x, y))$, and my problem was with $\psi_{2n}(x, y) = 0$. If $\psi_{n + 1}(x, y) = 0$ then $\phi_{n + 1}(x) = -\psi_n(x, y)\psi_{n + 2}(x, y)$, and if $\psi_{n - 1}(x, y) = 0$ then $\phi_{n - 1}(x) = -\psi_n(x, y)\psi_{n - 2}(x, y)$. Seems like now we have to deal with the cases when $\psi_{n + 2}(x, y)$ and $\psi_{n - 2}(x, y)$ are zero, in addition to $\psi_n(x, y)$?

Riccardo Brasca said:

Note that #10814 is labelled "awaiting author".

Yeah sorry about that! I've only realised the flaw in the multiplication-by-n proof after I made that PR, and now I'm worried that the PRs I've been opening might have been for naught. I'll go back to those once I have a valid argument.

Antoine Chambert-Loir said:

Schoof refers to Lang, Elliptic curves — Diophantine analysis.

AFAIK Lang does it by using properties of the Weierstrass $\wp$-function, which doesn't immediately generalise to non-zero characteristic, and I'm trying to avoid that.

[Antoine Chambert-Loir]

More precisely, Lang proves properties of the polynomials as elements of Z[X,Y] from the properties of the Weierstrass p-function, and it follows that it always hold, by specialization. By the way, that would also show the required properties for an elliptic curve in a non-Weierstrass form.

[Antoine Chambert-Loir]

For the first part, I mean that the addition formula for (n+1)P + (n-1)P gives you that it has some form, and the double of nP has some other form. Compare. (I did not check what it would give.)

[Kevin Buzzard]

@Antoine Chambert-Loir David is still struggling with this. Is the following true: if $R=\Z[a_1,a_2,a_3,a_4,a_6][1/\Delta]$ and $K$ is its field of fractions, and if $E/R$ is the universal elliptic curve, then any $K$-point of $E$ spreads out to an $R$-point?

[Amos Turchet]

Since E is separated and proper over R then the R-points of E are in bijection with the K-points of E (this is Poonen's book Theorem 3.2.13 - not 100% of the numbering since i don't have my physical copy with me). Is this enough?

[Kevin Buzzard]

But R is not a Dedekind domain -- it has dimension 6 or so.

[Antoine Chambert-Loir]

I don't have Bjorn's book on hand, but I suspect that would be the hypothesis of that theorem.

[Amos Turchet]

Fair enough, i was considering Z inverting \Delta and forgot that the coefficients are variables. My bad

[Amos Turchet]

Yes indeed you need Dedekind

[Antoine Chambert-Loir]

And I'm inclined to guess that David's expectation is wrong.

[Amos Turchet]

yeah if this is true there should be a reason if this works in this case since in general is false

[Antoine Chambert-Loir]

But it is very rare that you need that $K$-points extend to $R$-points in this setting, it is often enough that they extend to $R[1/D]$-points for some nonzero polynomial $D$, which is essentially trivial if $D$ is chosen correctly.

[Kevin Buzzard]

We are trying to make sense of the claim above that you can use Weierstrass P to prove all the theorems in the generic case and then deduce them for all elliptic curves.

[Kevin Buzzard]

David has [n](x:y:1)=(phi_n(x,y):omega_n(x,y):psi_n(x,y)) in the generic case and now we can't deduce it for every elliptic curve over every field because of this issue. What are we missing? I think this is the last missing step for getting division polynomials into mathlib.

[Antoine Chambert-Loir]

I guess the thing missing point is that if you have an equality of two points over a nonempty open subset of your $$\Spec(R)$$, then you have it everywhere.

[Kevin Buzzard]

But this doesn't even make sense if the sections don't spread out to the points missing from the open subset?

[Kevin Buzzard]

Aah, I see: the point is that [n](x:y:1) definitely spreads out, and so the other point does too.

[Antoine Chambert-Loir]

Can you spell out what you mean with "in the generic case"?

[Antoine Chambert-Loir]

Did David have a look at what Lang is doing on pages 37ff of Elliptic curves, Diophantine analysis?

[David Ang]

Yes I did

[Amos Turchet]

yes if you have two points that are equal generically and one of the spreads out than the other does too and the spreading out coincide (for the injectivity part you don't need the dedekind assumption)

[Kevin Buzzard]

If $A$ is $\Z[a_1,...,a_6,X,Y]/(Y^2+a_1XY...-a_6)$ and $L$ is its field of fractions then there's a "universal elliptic curve with a point" over $L$, with the point being $(X:Y:1)$. Here all the algebra works, the division polynomials are all elements of $L$, and the formula $[n](X:Y:1)=(\phi_n:\omega_n:\psi_n)$ is OK. The question he's asking me is how to get from this to the corresponding statement for all elliptic curves over all fields.

[Kevin Buzzard]

And the route he proposed was the following: we have this universal $\mathcal{E}$ over $L$ and then we have a random $E/k$ with a point $(x:y:1)$, and it would be nice to have a specialization map $\mathcal{E}(L)\to E(k)$ which is a group homomorphism, and then we'd be home.

[Kevin Buzzard]

But the issue is that in this generality it seems hard to define this group homomorphism, because $\mathcal{E}(L)$ might be strictly bigger than $\mathcal{E}(A)$

[Kevin Buzzard]

and mathlib doesn't have $\mathcal{E}(A)$ because $A$ isn't a field so the usual problems show up.

[Antoine Chambert-Loir]

Let me type as I think, I hope there won't be too much bs.

[Antoine Chambert-Loir]

One needs to find a valuation ring $R$ of $L$ lies above your $k$. Then you have $\mathcal E(K)=\mathcal E(R) \to \mathcal E(k)$.

[Kevin Buzzard]

My instinct now is not to define $\mathcal{E}(L)\to E(k)$ but instead just define the reduction map from the subgroup of $\mathcal{E}(L)$ generated by $(X:Y:1)$, and now you have to prove that reduction is a group homomorphism, which is probably going to be a nightmare because I'm not at all clear about which points can be reduced.

[Kevin Buzzard]

If you can find $R$ then this would be great.

[Antoine Chambert-Loir]

The existence of that $R$ is “standard”.

[Kevin Buzzard]

Oh great :-) So probably it's just rfl :-)

[Antoine Chambert-Loir]

Not quite ;-)

[Antoine Chambert-Loir]

It's basically the result by Chevalley that valuations extend. Take a maximal subring of $R$ which dominates $\operatorname{Spec}(k)$. It will be a valuation ring.

[Kevin Buzzard]

\Spec only exists locally in your LaTeX files :-)

[Kevin Buzzard]

It would be nice to have some global LaTeX macros set up! I am sick of writing \mathbb{Q} as well :-)

[Antoine Chambert-Loir]

Try \mathbf, it'll be nicer.

[Antoine Chambert-Loir]

Now, I don't believe that this is what Lang is suggesting, so there must be a simpler way to do that. Certainly, considering maximal subgroups is as useless as considering algebraic closures.

[Kevin Buzzard]

OK -- many thanks, I'm hoping this is the missing piece of the puzzle!

[Antoine Chambert-Loir]

In practice: you just need to have a good denominator that does not vanish where you want to evaluate your rational function.

[Kevin Buzzard]

Although I am now confused -- does the same technique then not prove the surely false result that if I have some smooth projective scheme of dimension >= 2 over a normal integral base then sections over the generic fibre extend to sections over the entire base?

[Antoine Chambert-Loir]

With enough too much handwaving, yes.

[Kevin Buzzard]

now I am worried all of a sudden because I don't immediately understand whether the problem (which I do not understand properly) will show up in the case of interest.

[Kevin Buzzard]

Oh, is the point that you can "extend a section to any point on the base" in some sense, but there's no guarantee that these extensions glue together?

[Antoine Chambert-Loir]

With the valuation ring game, the base is not the initial one, but an extremly blown-up one.

[Kevin Buzzard]

But you think it will be OK in David's application?

[Antoine Chambert-Loir]

Take $$[x: y:xy]\in\mathbf P_2(\mathbf Q(x,y))$. It does not extend to $\mathbf P_2(\mathbf Q[x,y])$, but there are large subrings on which it extends, for example, $\mathbf Q[x,y/x]$, and this subring dominates the closed point $(0,0)$ of $\operatorname{Spec}(\mathbf Q[x,y])$.

[Kevin Buzzard]

Antoine Chambert-Loir said:

Did David have a look at what Lang is doing on pages 37ff of Elliptic curves, Diophantine analysis?

What David claims seems to be the following. Let me distinguish between the "universal" case (one elliptic curve over $\Z[a_1,a_2,...,a_6][1/\Delta]$) and the "arbitrary" case (any elliptic curve over any field $K$, with $a_1,a_2,\ldots \in K$). In the universal case the literature is fine (modulo all the erroneous claims about the definition of $\omega_n$ which have been sorted out by David). Here $\phi_n,\psi_n,\omega_n\in\Z[a_1,a_2,a_3,a_4,a_6,X,Y]/(F=0)$. But moving from this to the arbitrary case where $a_i\in K$ and now $\phi_n,\omega_n,\psi_n\in K[X,Y]$ seems to be problematic. In the universal case the denominators $\psi_n$ are nonzero (because they're polynomials of degree $(n^2-1)/2$ or whatever) and there are no problems. In the arbitrary case you can have $\psi_n$ sometimes becoming zero, if the arbitrary point you're considering is a torsion point. According to David there is a gap in everyone's exposition here, because the formulas people use for the doubling formula etc all degenerate to stuff like $0/0$, and when trying to prove $[n](x:y:1)=(\phi_n:\omega_n:\psi_n)$ in the arbitrary case there are what he claims are genuine problems with the algebra: for example if $\psi_n(x,y)=0$ in $K$ then he doesn't know how to prove $[2n+1](x:y:1)=(\phi_{2n+1}(x,y):\omega_{2n+1}(x,y):\psi_{2n+1}(x,y))$. For example he cannot rule out that the RHS is not $(0:0:0)$, because you seem to completely lose control of all of the polynomials. There are variants $\tilde{\psi_n}\in K[X]$ where you remove some factor of $Y$ depending on whether $n$ is even or odd. If he could prove that $\tilde\psi_n\in K[X]$ and $\tilde\psi_{n+1}\in K[X]$ are coprime then he would be OK, or various other coprimality results, but he cannot do this because the proofs in the literature all rely on $[n](x:y:1)=(\phi_n:\omega_n:\psi_n)$ so the argument is circular (Silverman 1 has a coprimality statement in Ex 3.7(c) and then the claim about $[n](x:y:1)$ in part (d), but David has no idea how to do (c) without (d), and everyone else in the literature does (d) first, which David can't do for $2n+1$ if $\psi_n=0$). This is the obstruction which stops him making progress in the arbitrary case. So we have to argue in the universal case, where $\psi_n$ is provably nonzero, and then specialize. The problem now is the specialization is harder than you might think, again for the reason that you have to ensure that a random point in the universal case doesn't degenerate to $(0:0:0)$ again. David has looked at many sources (Lang, Silverman, Andrew Sutherland notes,...) but none of them seem to deal with this issue adequately.

[David Ang]

This summarises my issue succinctly. Note that I can't prove that the RHS (expressed in terms of division polynomials, be it in the universal or arbitrary case) lies on the curve, which would automatically rule out (0:0:0) (or singular points if we're willing to extend to Weierstrass curves), because that involves checking a massive ring equality e.g. with millions of monomials for n = 4.

[Adam Topaz]

Kevin Buzzard said:

Oh, is the point that you can "extend a section to any point on the base" in some sense, but there's no guarantee that these extensions glue together?

I'm coming to this discussion late, but I think the point is that you can extend a section to some blowup of the base, but the blowup may depend on the section. If you take a limit of all the blowups (aka the Zariski-Riemann space) then things work out, and that can be handled directly using valuation rings.

[Kevin Buzzard]

Right. Fortunately David only needs it for one point in the base. He'll still have to prove that the reduction map is a group hom, which I can imagine will be very fiddly in Lean. Even in the case of a DVR, and an elliptic curve over the field of fractions with good reduction, proving rigorously that the reduction map on points from the generic to the special fibre is a group hom is probably going to be messy.

[David Ang]

C.f. this message from another thread

[Adam Topaz]

So has the assertion you want been formalized over a valuation ring?

[David Ang]

Not yet. The current definitions we have for nonsingularity probably needs some tweaking before we do this.

[Antoine Chambert-Loir]

I've been trying to make sense of what Lang writes yesterday night, taking more or less notes. I'll come back with that in a few days. It's actually a bit hard to sort out between his “one can” and his “it is obvious that”…

[Junyan Xu]

Having thought about this, I'm not sure how the reduction homomorphism could help. To define the reduction homomorphism at the point $(\phi_n:\omega_n:\psi_n)$, you'd first remove a common factor (in a the valuation ring) and ensure one of $\phi_n$, $\omega_n$ and $\psi_n$ is a unit, and if the factor is not a unit, it means it evaluates to zero at the particular $a_1,\dots,a_6,x,y$, so $(\phi_n(x,y):\omega_n(x,y):\psi_n(x,y))=(0:0:0)$. So basically we need to show there's never a need to remove a common factor, and I don't see how working in the ring $\Z[a_1,a_2,a_3,a_4,a_6,X,Y]/(F=0)$ instead of a field could help with that ...

[Michael Stoll]

Can you show that $\phi_n$, $\omega_n$ and $\psi_n$ generate the unit ideal in the relevant ring (which is your ring localized at the discriminant of $F$)?

[Junyan Xu]

Generating the unit ideal is equivalent to not being contained in any maximal ideal, which is equivalent to images not simultaneously vanish under any homomorphism to a field. So we ought to be able to prove that. Maybe there's some way to prove using induction + computation, but I don't see how yet.

Correction: I think reduction needs to be done in the projective coordinates, so we probably want tot show $\phi_n\psi_n, \omega_n$ and $\psi_n^3$ generates the unit ideal instead, which is equivalent to that $\omega_n$ and $\psi_n$ generate the unit ideal.

[Michael Stoll]

Essentially, you want to wirte a power of the discriminant as a linear combination of the polynomials. There should be some recurrence for that...

[David Ang]

I believe this reduces to computing the resultant, which is precisely the thing that I'm unsure how to do.

[Junyan Xu]

Something don't quite check out, and I'm no longer sure what we are supposed to prove. Silverman's (d) doesn't specify what we're supposed to do when $\psi_m(P)=0$. And I think we have to do something more sophisticated at least in characteristic two because we have $\psi_{2m}=2\psi_m\omega_m$ so it vanishes identically in char 2, but it's not true that the double of every point is infinity. see below

unnamed-1.png
unnamed.png

[David Ang]

Note that Silverman's definition of $\omega_m$ is wrong in characteristic two.

[Junyan Xu]

The polynomials have coefficients in Z and can specialize to any characteristic. I think you mean that when we have $a_1$ and $a_3$ in the Weierstrass equation then we need to define $\omega_m = \dfrac{\psi_{2m}}{2\psi_m} - \dfrac{1}{2}\psi_m(a_1\phi_m + a_3\psi_m^2)$.

[David Ang]

Yes, we have to first work in the universal ring to define the polynomials, then specialise it when necessary.

[Jz Pan]

Just FYI, did you check the definition of division polynomial in Pari/GP or Sage? You can first look at their documentation, to see if they implemented characteristic 2 case. In Sage's documentation there is another reference different from Silverman.

[Junyan Xu]

This definition of $ω$ is correct, but it takes some effort to show it's coefficients are in $\mathbb{Z}$ without 2 in the denominator. It's proven in my notes which contains a purely algebraic proof of the fact that $[n](x:y:1)=(\phi_n(x,y):\omega_n(x,y):\psi_n(x,y))$ and intend to serve as a blueprint for formalization. It's a much more refined and detailed version than my Zulip DMs with @David Ang but still in draft form.

The proof is based on the observation that in Jacobian coordinates, two (mutually exclusive) formulas, one for $P=Q$ and one for $P≠ Q$, suffice to cover all cases of the group law, which allows us to do induction in two cases $P_n+P_n$ and $P_n+P_{n+1}$, which is implicit in Sutherland's notes. The whole proof that I found is much longer and nontrivial than the notes suggest though, and some arguments involving polynomial substitutions may be tricky to formalize, and the biggest computation requires verifying two expressions of 5387 terms are identical. At the end of Section 1 I outlined how we could switch to a complex analytic proof (we're verifying polynomial identities and the universal ring (polynomial ring modulo Weierstrass polynomial) is in char 0 and embeds into the complex numbers), which might be easier to formalize but maybe an algebraic proof is still desirable for import/modularity reasons.

[Junyan Xu]

One fact used in my proofs is that the division polynomials form an elliptic sequence, for which an algebraic proof is also lacking in the literature. I managed to discover one, and it involves some crazy identity of 11 terms. Does anyone recognize this?

[David Ang]

Jz Pan said:

Just FYI, did you check the definition of division polynomial in Pari/GP or Sage? You can first look at their documentation, to see if they implemented characteristic 2 case. In Sage's documentation there is another reference different from Silverman.

I haven’t checked PARI, but the definitions of $\psi_n$ and $\phi_n$ in Sage agree with mine. They compute the Y-coordinate in Sage differently, and in particular they did not provide a closed form for $\omega_n$.

[Jz Pan]

David Ang said:

in particular they did not provide a closed form for $\omega_n$.

Neither in PARI:

2024-05-08-023413.png

[Jz Pan]

I happed to have an ancient note about division polynomials I written in about 10 years ago when learning Silverman's book, in Chinese. I could quickly translate it into English, hopefully it will be useful for you.

[David Ang]

I’m OK with Chinese :)

[Jz Pan]

Here is it: T-EC-divpol.pdf. Hopefully it's useful to you. I was checked 10 years ago that all of division polynomials are well-defined. But maybe the details are lacking or are incorrect in this note.

[Jz Pan]

I reread the definition in my note. Seems that it's best to shift the definition of $\psi_{2n}$ as $\widetilde\psi_{2n}:=\psi_{2n}/\psi_2$ as in PARI.

[Jz Pan]

2024-05-08-042938.png

Maybe the $\omega_{2n+1}$ should be shift similarly as $\widetilde\omega_{2n+1}:=\omega_{2n+1}/\psi_2$. In this case all the $\psi,\omega,\phi$ are in the polynomial ring $\mathbb{Z}[b_2,b_4,b_6,b_8,x]$.

[Junyan Xu]

Silverman's definition of $\omega_n$ is missing the $\dfrac{1}{2}\psi_m(a_1\phi_m + a_3\psi_m^2)$ terms. Defining $\psi_n$ (docs#normEDS') in terms of $\widetilde\psi_n$ (docs#normEDS'') is the approach taken in mathlib. You do need the $\psi_2$ factor to make an elliptic divisibility sequence though.

[Jz Pan]

Junyan Xu said:

Silverman's definition of $\omega_n$ is missing the $\dfrac{1}{2}\psi_m(a_1\phi_m + a_3\psi_m^2)$ terms.

I see. Thanks for the information.

[Jz Pan]

Your definition scares me a little bit since both of the denominator contain 2...

[Jz Pan]

Do you mean $\omega_m:=(\psi_{m-1}^2\psi_{m+2}-\psi_{m+1}^2\psi_{m-2})/\psi_2$ is not correct, either?

[Junyan Xu]

Jz Pan said:

Do you mean $\omega_m:=(\psi_{m-1}^2\psi_{m+2}-\psi_{m+1}^2\psi_{m-2})/\psi_2$ is not correct, either?

Yeah, that's equal to $\psi_{2m}/\psi_m$, so it's missing a 1/2, and also missing the two terms $\dfrac{1}{2}\psi_m(a_1\phi_m + a_3\psi_m^2)$.

[Junyan Xu]

The doubling formula in Jacobian coordinate is here (with negY defined here), which demands that $\psi_{2m}=\psi_m(2\omega_m+a_1\phi_m\psi_m+a_3\psi_m^3)$ (the expression in the parentheses is the homogenization of $\psi_2=2y+a_1 x+a_3$, applied to $(\phi_m:\omega_m:\psi_m)$.

[Junyan Xu]

The proof that $\omega_n$ has integer coefficients is in Section 3 of my notes, specifically page 14.

[Jz Pan]

Oh, I remembered. Silverman's $\omega_n$ only computes $\psi_2([n]P)$, so you can't recover the y-coordinate for char 2 :sweat_smile:

[Junyan Xu]

I'm not sure what you mean? Silverman's formula is correct if $a_1=a_3=0$ and incorrect otherwise. In char 2 if $a_1=a_3=0$ then the curve is singular, but the formula still apply to nonsingular points.

[Jz Pan]

I mean this

2024-05-08-053721.png

Notice the red circle, its $\psi_2$ but not $y$

[Jz Pan]

And I think that is correct regardless of characteristic. The disadvantage is that you can't say anything about y using this for char 2.

[Junyan Xu]

That sounds right. But part (d) of the exercise does ask to show the y coordinate is given by $\omega_m$:
image.png

[Junyan Xu]

How did you come up with the correct statement (with $\psi_2$ instead of y)?

[Jz Pan]

Junyan Xu said:

How did you come up with the correct statement (with $\psi_2$ instead of y)?

I didn't remembered. Maybe it's natural to consider $\psi_2$ when I found that y is not correct (the correct formula is in the yellow circle):

2024-05-08-061051.png

I think I checked n=2 case using computer algebra system (blue circle).

[Jz Pan]

I gave up at that time finding the correct $\omega$ for y after seeing that yellow circle even for n=2 case, :sweat_smile:

[Junyan Xu]

Apparently David discovered the correct formula in an old paper (which is also a major inspiration of my proofs).

[Jz Pan]

By the way, I think we still can say something on E[n] without knowing the correct $\omega_n$? For example, I think we still can prove that E[n] is of size n^2 if n is invertible in that field, by knowing that the roots of $\psi_n$ are all the x-coordinates of E[n], then counting the number of solutions of quadratic equation for each x.

[Jz Pan]

Junyan Xu said:

Apparently David discovered the correct formula in an old paper (which is also a major inspiration of my proofs).

I see. That's the French paper referenced in your note.

In fact if you believe the correct $\omega_n$ exists, then it's not hard to discover, if you know that Silverman's $\psi_{2n}/\psi_n$ computes $\psi_2=2y+a_1x+a_3$ (as in my note points out). Subtract $a_1x+a_3$ from it (the x is also computed by a division polynomial known in Silverman's), then divide by 2, you get that formula. But who dares to divide 2 in characteristic 2 case? :joy:

[Junyan Xu]

Gladly we can define the polynomials (and prove facts about them) in char 0 (in the polynomial ring over Z, the universal ring or even the field of fractions), and they continue to apply in char 2. Indeed some of the arguments in my notes involve division by $\psi_n$ so need to be carried out in the field of fractions in char 0. If you do it in char p, the leading term of $\psi_{pn}$ becomes zero and it's not clear how to show $\psi_{pn}$ is nonzero.

[David Ang]

Jz Pan said:

By the way, I think we still can say something on E[n] without knowing the correct $\omega_n$? For example, I think we still can prove that E[n] is of size n^2 if n is invertible in that field, by knowing that the roots of $\psi_n$ are all the x-coordinates of E[n], then counting the number of solutions of quadratic equation for each x.

How do you do this directly? I can write down an explicit injection from the x-coordinates of $E[2]$ to the roots of $\psi_2$ that's surjective over a sufficiently large extension. For general $n$ you'd need to do it inductively, and I don't see a way to avoid the addition/doubling formula, which in turn requires knowing the other coordinates.

[Jz Pan]

David Ang said:

How do you do this directly?

I forgot the exact details; hopefully you can find all of them in my notes <https://leanprover.zulipchat.com/user_uploads/3121/oJbbONEPnsNRmp66St2_vhQN/T-EC-divpol.pdf> if it was correct.

[Jz Pan]

Junyan Xu said:

it's not clear how to show $\psi_{pn}$ is nonzero.

I proved that all $\psi_n$ are nonzero, via proving that the images of $\phi_n$ and $\psi_n^2$ in
$K[x]\subset K(E)$ are coprime. In my note it writes "the details are omitted" but now I can't remember the details...

[EDIT] But why in the next paragraph I wrote "We should also show that for any
$m\neq 0$, the image of $\psi_m$ in $K(E)$ is not zero" again :man_facepalming: Isn't it a consequence of "the images of $\phi_n$ and $\psi_n^2$ in
$K[x]\subset K(E)$ are coprime"?

[Junyan Xu]

Just read your notes and I think I rediscovered a great deal of what you did. You also discovered that $6x^2+b_2 x+b_4$ from Somos recurrence. Your observation that many polynomials only involves $b_i$ without the need to reduce to $a_i$ is nice and may be used cut down the 5387 terms. Your proposition 0.1 is quite interesting and may be able to simplify my proofs of the $A_X, A_Y$ identities.

You observed that $E(m,n,r,0)$ follows from $E(m,n,1,0), E(m,r,1,0)$ and $E(n,r,1,0)$, and you seem to have a different proof that $E(m,n,1,0)$ follows from the defining (even-odd) recursion which doesn't involve half-integers, by first proving the Somos 4 case ($E(n,2,1,0)$).

[Junyan Xu]

Regarding the verification of the 5387-term identity: switching from $a_i$ to $b_i$ indeed reduces $\psi^c_4$ to 378 terms and $\psi^{ch}_2(P_2)$ to 386 terms. But their difference still has 369 terms, and factors as $b_4^2-b_2 b_6+b_8$ times a sum of 180 terms, and if you expand $b_4^2-b_2 b_6+4b_8$ into $a_i$ you get zero. I thought the $b_i$'s are algebraically independent but in fact they are not ($b_2,b_4,b_6$ are probably algebraically independent?)
Since we're in char 0 for verification of the identity, we can write $b_8=(b_2 b_6-b_4^2)/4$, and then both sides have 286 terms only.

[Ruben Van de Velde]

"only"

[David Ang]

That’s pretty much the ballpark of being ring-able in Lean

[Junyan Xu]

I have figured out a substantial simplification of the proof. Instead of verifying the four identities (AX,AY,DX,DY), we instead directly attack the identity $nP=(\phi_n:\omega_n:\psi_n)$ in the field of fraction of the universal ring, for which we can use n+1 induction rather than the 2n / 2n+1 induction. The end of my Section 4 basically shows two things: $(x(Q)-x(R))^2(x(R-Q)-x(R+Q))=\psi_2(Q)\psi_2(R)$, and $(x(Q)-x(R))\psi_2(Q+R)+(x(Q)-x(Q+R))\psi_2(R)+(x(Q+R)-x(R))\psi_2(Q)=0$ if Q and R has different x-coordinates. If you take Q=nP and R=P where P=(X,Y) is the universal point, then Q and R has different x-coordinates for all n > 1 (requires some proof but it's essentially the fact that $\psi_n$ is nonzero modulo Weierstrass equation), and by these formulas you can compute the coordinates of (n+1)P from the coordinates of nP, P, and (n-1)P, which by induction can be assumed to be given by $(\phi:\omega:\psi)$. To show (n+1)P is also given by $(\phi:\omega:\psi)$, it suffices to prove certain identities between $\phi,\omega,\psi$ which is essentially what I did in the end of Section 4. We are left to check the $n=1$, i.e. the doubling formula, and very little computation is required for that.

[David Ang]

Proving the identity in the universal ring means we have to apply a specialisation map to get the identity on an arbitrary curve, which requires defining the reduction map etc and that's a lot of work as per the discussion before?

[Junyan Xu]

The end of my Section 1 shows how to reduce to the universal case (or the complex case). This reduction step still require the 2n / 2n+1 induction, and rely crucial on the observation that two formulas suffice in Jacobian coordinates. Maybe I should supply some more details though; it may not be clear how those "force" work.

[Junyan Xu]

Basically, the addition formulas in Jacobian coordinates (some integer coefficient polynomials) that hold universally over any field of any characteristic show that we just need to prove six polynomial identities (5a-6c) (modulo Weierstrass equation) to show that $nP=(\phi_n(x,y):\omega_n(x,y):\psi_n(x,y))$ holds over any field.
image.png

The formula (5c) and (6c) hold basically by definition. Now, if the universal formula $n(X,Y)=(\phi_n:\omega_n:\psi_n)$ holds, I claim that (5a,5b,6a,6b) also hold. This is because the addition and doubling formulas is valid over any field, in particular the field of fraction of the universal ring, so e.g. $(D_X(\phi_n,\omega_n,\psi_n):D_Y(\phi_n,\omega_n,\psi_n):D_Z(\phi_n,\omega_n,\psi_n))=2(n(X,Y))$ must be equal to $(2n)(X,Y)=(\phi_{2n}:\omega_{2n}:\psi_{2n})$. Since (6c) says the z-coordinates agree, the x and y coordinates must also agree, i.e. (6a) and (6b) also hold. The case of (5a-5b) is similar.

[Junyan Xu]

Just submitted a paper review and I'll start formalizing the proofs soon. I think I'll focus on reducing the general case to the universal case initially; the next would be the proof of elliptic relations, and then Somos sequence stuff and integrality of $\omega_n$ (I think #6703 / #10878 may need some rewrites, and I prefer names like WeierstrassCurve.DivisionPolynomial.psi), and finally the two formulas in affine coordinates to settle the universal case.

If @David Ang got some time maybe he'll update #9405 and prove that two formulas suffice in Jacobian coordinates. (This is all in page 11 of my notes.)

[Junyan Xu]

#12874 (now builds) is an easy naming convention compliance PR, to avoid perpetuating two capitalization errors, in preparation for the Jacobian group law PR #9405.

[Junyan Xu]

Thanks to @Kim Morrison for merging #12874 and @David Ang for reviewing #12883. Since I've now defined the universal elliptic curve and the canonical distinguished point on it and it adds more materials to the files touched by #12883, I think I might close it and open a new PR when the time is ripe, but I'll make sure I incorporate the suggestions there.

[Junyan Xu]

Since David needs some time to clean up #9405, I've been focusing on proving normEDS gives elliptic divisibility sequences using my algebraic argument, which is half complete as of now, and I think I have an argument for the converse too, assuming $\psi_1\psi_2$ is not a zero divisor. I believe that the "divisibility" part only requires $\psi_1\mid\psi_2\mid\psi_4$ and $\psi_1\mid\psi_3$ on top of ellipticity, with the same non-zero-divisor assumption.

[Junyan Xu]

I've been focusing on proving normEDS gives elliptic divisibility sequences using my algebraic argument

The proof is complete at #13057. Some more results are to be added before I mark it awaiting-review, but you're welcome to take a look beforehand.

[Junyan Xu]

I managed to define the $\omega$ polynomials without division (by 2 or whatever) and show it satisfies the desired property $\psi_n(2\omega_n+a_1\phi_n\psi_n+a_3\psi_n^3)=\psi_{2n}$:
image.png

It amounts to the following expression:
$\omega_n:=\frac{\psi_{n+1}\psi_n\psi_{n-1}}{\psi_3\psi_2}\left(\psi_3(a_1 F_Y-F_X)+4F(2F+\psi_2^{2(1)})\right)-\frac{\psi_{n-2}\psi_{n+1}^2}{\psi_2}+(Y-F_Y)\psi_n^3$
where $\psi_2^{2(1)}=4X^3+b_2 X^2+2b_4 X+b_6$ is the single-variable equivalent of $\psi_2^2$, $F$ is the Weierstrass polynomial, and $F_X$ and $F_Y=\psi_2$ are its derivatives ($Y-F_Y$ is also known as negPolynomial); the term $4F(2F+\psi_2^{2(1)})$ can be completely omitted without affecting evaluation on points on the curve, so the expression can be simplified to $\frac{\psi_n\psi_{n-1}-\psi_{n-2}\psi_{n+1}}{\psi_2} \psi_{n+1}(a_1 F_Y-F_X)+(Y-F_Y)\psi_n^3$, but I choose to make the definition equal to the common definition in the literature.

I defined $\frac{\psi_{n+1}\psi_n\psi_{n-1}}{\psi_3\psi_2}$ and $\frac{\psi_{n-2}\psi_{n+1}^2}{\psi_2}$ in a division-free way (as polynomial expressions in the initial values b,c,d of normalized elliptic divisibility sequences), without using choice to select witness of divisibility, so $\omega$ would be computable if Finsupp/Polynomial are refactored to be computable (recent attempt in #12922).

The definition for $\frac{\psi_{n+1}\psi_n\psi_{n-1}}{\psi_3\psi_2}$ involves a split into six cases, and the proof is a bit cumbersome now, so please let me know if you have smart ways to simplify it. The PR #13057 is ready for review and contains I believe all ingredients about EDSs that are required for the formula for $nP$.

My original plan was to prove the universal $2\omega_n=\psi_{2n}/\psi_n-a_1\phi_n\psi_n-a_3\psi_n^3$ has even coefficients, divide all coefficients by 2 (integer division is also computable), and then specialize, but I later realized I can work out an explicit expression that works in any comm. ring, so why not.

By the way, I have been using the Supermaven VSCode extension for code completion for 1-2 weeks by now, which is an alternative of GitHub Copilot with a free tier, and I find it certainly saves a lot of copypasting + editing for generating boilerplate API lemmas once there are a few similar ones around.

[Junyan Xu]

My definitions of the division polynomials are in this file, which is separate from @David Ang's definition in #10878 (and #6703), but it should be easy to show both definitions are congruent modulo $F$.

[David Ang]

Ah, I forgot #6703 existed! I'll update it now.

[David Ang]

Maybe let's try to unify the definitions in that PR and get it merged first before your massive #13057? I honestly much prefer your naming of ψ, φ, ω, etc. I just wasn't sure if this is a good naming convention in mathlib, so resorted to the chunky divisionPolynomialX, divisionPolynomialY, divisionPolynomialZ, etc.

[Junyan Xu]

My current definition of $\omega$ uses extensive theory about normalized EDSs in #13057, mostly importantly that it's a divisibility sequence (and also explicit witnesses of divisibility). If you just want to get $\psi$ and $\psi$ in then current mathlib/master should be enough for that.

I think the names ψ, φ, ω are standard and reasonable to put under Weierstrass namespace; we already have standard expressions derived from a Weierstrass curve under the same namespace, like b₄, c₆ etc. Since ψ, φ are common variable names (for morphisms I think), I currently protect them but they can still be convenient accessed through dot notation. To develop basic APIs about them I'd like to rewrite by their definitions, so I do open WeierstrassPolynomial (ψ φ) etc. to make rw [φ, ψ] work.

[Kevin Buzzard]

Yikes -- #13057 is +1000 lines! Can it be broken up into smaller things?

[Junyan Xu]

I think it can be relatively cleanly split into an "elliptic" part and a "divisibility" part; let me do that later today.

[Ruben Van de Velde]

It seems like everything outside the main file could easily be reviewed by people without expert knowledge (e.g. me), so it would be nice to split that out as well

[Junyan Xu]

I've split off two PRs: #13153 (auxiliary results) and #13155 (first part of the main file)

However, there's currently a strange "check the cache" CI failure (thread)

[Kim Morrison]

Not sure about the cache failure. Perhaps merge master and try again??

[Junyan Xu]

I've retried failed jobs twice, and every time it appears to successfully upload the cache, download the cache, and unpack it, but then emit an error with exit code 3.
The branch is new and I need to wait for new commits to land in master to merge it.

[Junyan Xu]

Merged master and it seems the issue persists ... (update: after some more merges the error finally went away)

[Junyan Xu]

The reduction to the universal case is done, thanks to @David Ang's updated Jacobian PRs culminating in #9405, and this is the only remaining sorry that matters. These affine formulas plus some proven identities (e.g. smulX_sub_smulX) will be needed to close the sorry.

The final statement is:

variable {F : Type*} [Field F] (W : WeierstrassCurve F)
theorem smul_eq_divisionPolynomial_eval {x y : F} (h : Affine.Nonsingular W x y) (n : ℤ) :
    (n • Point.fromAffine (Affine.Point.some h)).point = ⟦smulEval W x y n⟧

where

abbrev smulEval (n : ℤ) : Fin 3 → R := evalEval x y ∘ ![W.φ n, W.ω n, W.ψ n]
abbrev evalEval [Semiring R] (x y : R) (p : R[X][Y]) : R := eval x (eval (C y) p)

[Kevin Buzzard]

So are you close to "the p-torsion of an elliptic curve over Qbar has p^2 elements"?

[David Ang]

Yes!

[Kevin Buzzard]

We definitely need that for Fermat :-)

[David Ang]

@Junyan Xu I'm extracting small PRs from your large ones and I noticed that preNormEDS'_odd/even etc can be generalised to all integers somewhat easily:

lemma preNormEDS'_odd (m : ℤ) : preNormEDS' b c d (2 * m + 1) =
    preNormEDS' b c d (m + 2) * preNormEDS' b c d m ^ 3 * (if Even m then b else 1) -
      preNormEDS' b c d (m - 1) * preNormEDS' b c d (m + 1) ^ 3 * (if Even m then 1 else b)

This obviously follows from the EDS recurrence, but do you need this in the proof (or have you done this somewhere)?

[Junyan Xu]

Do you mean preNormEDS? preNormEDS' is the Nat-indexed version, where subtraction makes little sense. preNormEDS_odd/even can be generalized in the way you propose, but the subtraction-free Nat version is likely useful for inductive proofs, given the form of normEDSRec (you'd need to rewrite by ↑(n + 2) - 1 = ↑(n + 1) (where the coercion is from Nat to Int) in order to use your proposed preNormEDS_odd above, for which you need a somewhat powerful tactic (omega IIRC). I originally proposed a form of normEDSRec that takes a Int-indexed sequence but you changed it to the Nat-indexed version, so lemmas would be better be compatible with it.

[David Ang]

Do you think we should revert to your Int-indexed normEDSRec? You also made a good point in that PR that we don't need an Int-indexed version since we can just use negInduction (more appropriately called negRec).

[Junyan Xu]

I think there's no pressing need to revert it. If you do you need to fix #13057 (there are now two applications of normEDSRec

It may not too painful to work with the generalized version you propose; my EvenRec and OddRec in #13057 are defined like what you propose, and in IsEllSequence.normEDS_of_mem_nonZeroDivisors I'm basically proving the generalized version from the current version of normEDS_even/odd (albeit only for large enough integers, not all integers).

I think it's probably best to have the generalized Int-versions (more symmetrically centered around m and m+1) in addition to the Nat-versions (centered around m+2 and m+3) which directly follow from the recursive definition.

[Junyan Xu]

The formula has been fully proven in #13782, which is +2,429 -217 in total and currently split into 7 dependent PRs. The strategy of proof and all the reductions are described in the module docstring.

• #13399 was authored by @David Ang and approved by me, but currently seems to be blocked due to a question of @Johan Commelin.

• #12883 was written by me and reorganized by David. It moves things around, but as the bot confirms only adds four lemmas and an instance.

• The Jacobian coordinate PRs by David are fully merged, but I have some additions in #13846.

• The universal elliptic curve is added in #13847 as a separate file, which depends on the new Polynomial/Bivariate file added in the affine formulas PR #13845 (both awaiting CI).

• #13155 is about elliptic divisibility sequences and based on my proof on Math.SE and I'll probably wait for David to review it, since he has read the proof. #13057 builds on top of it.

[Yaël Dillies]

I've reviewed the first three and #13845 but I am no expert

[Ruben Van de Velde]

If you have time for reviews now, @Yaël Dillies ... :innocent:

[Yaël Dillies]

I am reading #queue unless you tell there's something better to do with my time!

[Michael Stoll]

What about the disentangling order and algebra refactor? :innocent:

[Yaël Dillies]

Oh I need like a week straight available for that one...

[Junyan Xu]

In #13845 I'm introducing a new file for bivariate polynomials, including two scoped notations R[X][Y] and Y originally in EllipticCurve/Affine, however there are some disagreement regarding the name of the scope: the original name was PolynomialPolynomial, and @Yaël Dillies suggested Polynomial2. Polynomial is also a reasonable scope, since all lemmas are still in the Polynomial namespace, which is also the namespace of Polynomial.X and the scope of the notation R[X].

I somewhat sympathize with the Polynomial2 suggestion because it's more scalable in case we want to use R[X][X][X] for trivariate polynomials, but @David Ang thinks that evalEval should then be renamed to eval2, which I think is too confusing given the existence of Polynomial.eval₂. Therefore I'm now making a poll here for the name of the scope and the name of the evaluation map that takes x y : R and p : R[X][Y] and returns p evaluated at X=x and Y=y:

[Junyan Xu]

/poll
Polynomial, evalEval
PolynomialPolynomial, evalEval
Polynomial2, evalEval
Polynomial2, eval2
Polynomial, eval2
PolynomialPolynomial, eval2

[Junyan Xu]

I'm using the first option currently. I've also thought about

abbrev Polynomial2 (R) [Semiring R] := R[X][Y]

and then Polynomial.evalEval could potentially be renamed Polynomial2.eval. But when you want to apply Polynomial.eval to a Polynomial2 you'd need some Polynomial2.toPolynomial, and I think it's not good practice to have two different dot notation that could apply on reducibly defeq types. (I don't want to make the abbrev a def instead, because I don't think it should have all instances on R[X][Y] and shouldn't be regarded as a separate new type.)

[Johan Commelin]

I like the idea of eval2. Is there a better name for eval₂? aeval is already taken. Maybe eval_h, because it takes a hom as extra argument? Or evalh or heval?

[Jz Pan]

What about evalTwo?

[Junyan Xu]

If you change the name of (Mv)Polynomial.eval₂(RingHom), 183 defs/lemmas will need to be deprecated according to Loogle.

[Filippo A. E. Nuccio]

I fear that going for the namespace Polynomial would break the actual neat distinction between Polynomial and MvPolynomial, hence my preference for Polynomial2.

[David Ang]

I am indifferent about whether we use Polynomial/PolynomialPolynomial or Polynomial2, but I strongly prefer the corresponding eval name to match this choice.

[David Ang]

Alternatively we could do BvPolynomial for bivariate polynomials

[Junyan Xu]

#13846 and #13845 (except for the naming issue) have been approved by @David Ang. Regarding the naming issue there are many suggestions but not many votes. It seems that we haven't reached consensus regarding the optimal name, but if we can at least agree that the current names (Polynomial, evalEval) are acceptable, I suggest that we merge #13845 now.