feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group law for Jacobian coordinates #9405
Conversation
Multramate
added
WIP
Multramate
added
blocked-by-math-PR
Multramate
changed the title
…acobian.Representative
…ve.Jacobian.Point
|
So do you want both types of coordinates in Mathlib? What is the motivation for doing it that way, rather than just choosing one type of coordinates? |
I need Jacobian coordinates, because their coordinates are precisely the division polynomials in #6703 and the phi_n/omega_n defined in AEC Exercise III.3.7, albeit with an error. I don't need projective coordinates at the moment, but I believe it might be a very useful definition in general (e.g. to give an elementary definition of reduction modulo p without any bias on the weights). In fact projective coordinates was my toy model for Jacobian coordinates because originally I wasn't sure how to write the API at all. |
…nd nonsingularity for Jacobian coordinates (#9432) Define a Jacobian point representative over a ring `R` as the type `Fin 3 -> R`, and its equivalence class `PointClass` as a quotient by the usual weighted scaling relation. Define the analogous `equation` and `nonsingular` predicates on `Fin 3 -> F` over a field `F`, and lift `nonsingular` to `PointClass`. This also has minimal API (e.g. it's missing many of the `equation` lemmas) as most computations should ideally be done using the affine API. This is the first in a series of four PRs leading to #9405 and is analogous to #9416
leanprover-community-mathlib4-bot
added
the
merge-conflict
…nd nonsingularity for Jacobian coordinates (#9432) Define a Jacobian point representative over a ring `R` as the type `Fin 3 -> R`, and its equivalence class `PointClass` as a quotient by the usual weighted scaling relation. Define the analogous `equation` and `nonsingular` predicates on `Fin 3 -> F` over a field `F`, and lift `nonsingular` to `PointClass`. This also has minimal API (e.g. it's missing many of the `equation` lemmas) as most computations should ideally be done using the affine API. This is the first in a series of four PRs leading to #9405 and is analogous to #9416
…nd nonsingularity for Jacobian coordinates (#9432) Define a Jacobian point representative over a ring `R` as the type `Fin 3 -> R`, and its equivalence class `PointClass` as a quotient by the usual weighted scaling relation. Define the analogous `equation` and `nonsingular` predicates on `Fin 3 -> F` over a field `F`, and lift `nonsingular` to `PointClass`. This also has minimal API (e.g. it's missing many of the `equation` lemmas) as most computations should ideally be done using the affine API. This is the first in a series of four PRs leading to #9405 and is analogous to #9416
…nd nonsingularity for Jacobian coordinates (#9432) Define a Jacobian point representative over a ring `R` as the type `Fin 3 -> R`, and its equivalence class `PointClass` as a quotient by the usual weighted scaling relation. Define the analogous `equation` and `nonsingular` predicates on `Fin 3 -> F` over a field `F`, and lift `nonsingular` to `PointClass`. This also has minimal API (e.g. it's missing many of the `equation` lemmas) as most computations should ideally be done using the affine API. This is the first in a series of four PRs leading to #9405 and is analogous to #9416
…nd nonsingularity for Jacobian coordinates (#9432) Define a Jacobian point representative over a ring `R` as the type `Fin 3 -> R`, and its equivalence class `PointClass` as a quotient by the usual weighted scaling relation. Define the analogous `equation` and `nonsingular` predicates on `Fin 3 -> F` over a field `F`, and lift `nonsingular` to `PointClass`. This also has minimal API (e.g. it's missing many of the `equation` lemmas) as most computations should ideally be done using the affine API. This is the first in a series of four PRs leading to #9405 and is analogous to #9416
…nd nonsingularity for Jacobian coordinates (#9432) Define a Jacobian point representative over a ring `R` as the type `Fin 3 -> R`, and its equivalence class `PointClass` as a quotient by the usual weighted scaling relation. Define the analogous `equation` and `nonsingular` predicates on `Fin 3 -> F` over a field `F`, and lift `nonsingular` to `PointClass`. This also has minimal API (e.g. it's missing many of the `equation` lemmas) as most computations should ideally be done using the affine API. This is the first in a series of four PRs leading to #9405 and is analogous to #9416
|
I'd like to merge master into this soon, because I'm building on top of this branch but |
|
Sure, give me a couple of hours and I'll hopefully update everything by today! |
|
Thanks! |
…acobian.Representative
…ve.Jacobian.Point
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| def dblX (P : Fin 3 → R) : R := | ||
| (3 * P x ^ 2 + 2 * V.a₂ * P x * P z ^ 2 + V.a₄ * P z ^ 4 - V.a₁ * P y * P z) ^ 2 | ||
| + V.a₁ * (3 * P x ^ 2 + 2 * V.a₂ * P x * P z ^ 2 + V.a₄ * P z ^ 4 - V.a₁ * P y * P z) * P z | ||
| * (P y - V.negY P) - V.a₂ * P z ^ 2 * (P y - V.negY P) ^ 2 - 2 * P x * (P y - V.negY P) ^ 2 |
There was a problem hiding this comment.
What do you think about replacing the appearances of the RHS of WeierstrassCurve.Jacobian.eval_polynomialX by the LHS in this definition and in dblY below? We could replace P y - V.negY P with the evaluation of polynomialY too, but that wouldn't be shorter.
|
Here are some additions and changes I made to the Jacobian file for the purpose of division polynomials, and maybe you want to incorporate them into one or more of your PRs. I still think it makes sense to merge this PR as a whole and close the others. |
|
Thanks! I'll have a look later in the week. I don't mind merging this PR as a whole, but I don't want to set a precedent where 1000+ line feat PRs are acceptable. Maybe we can do this for |
Completes the proof of the group law in Jacobian coordinates, analogously to #8485