mathlib4

mathlib4 copied to clipboard

Completes the proof of the group law in Jacobian coordinates, analogously to #8485

• [x] depends on: #9432
• [ ] depends on: #9433
• [ ] depends on: #9435
• [ ] depends on: #9436
• [ ] depends on: #13060

Jan 02 '24 22:01 Multramate

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?

Jan 09 '24 14:01 alexjbest

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.

Jan 09 '24 14:01 Multramate

I'd like to merge master into this soon, because I'm building on top of this branch but WeierstrassCurve.map is not available here. I expect this PR to be merged as a whole so I won't update the "prerequisite" PRs. Before I merge I'd like to get #12874 in.

May 13 '24 20:05 alreadydone

Sure, give me a couple of hours and I'll hopefully update everything by today!

May 13 '24 20:05 Multramate

Thanks!

May 13 '24 20:05 alreadydone

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.

May 27 '24 19:05 alreadydone

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 Projective once the Jacobian ones are done.

May 27 '24 19:05 Multramate

@alreadydone do we actually need these?

lemma addZ_self {P : Fin 3 → R} : addZ P P = 0
lemma addX_self {P : Fin 3 → R} (hP : V.Equation P) : V.addX P P = 0
lemma addY'_self {P : Fin 3 → R} : V.addY' P P = 0
lemma addY_self {P : Fin 3 → R} (hP : V.Equation P) : V.addY P P = 0

Looks to me that they should never be accessed if we're using add.

May 28 '24 17:05 Multramate

Those addXYZ_self lemmas were mainly introduced to prove addXYZ_smulField for all m,n (by the way the branch is now sorry free). It's equally valid in the m=n case, and although it's just a lemma towards the main theorem it could be useful elsewhere.

The generalization of scalar multiplication on Fin 3 → R from Rˣ to R is for the same purpose; it would be ugly to use Units.mk0, which still won't cover the m=n case. Although the case n=m+1 suffices for the main theorem, it's nicer to state and prove the general case.

May 31 '24 04:05 alreadydone

This PR/issue depends on:

• ~~leanprover-community/mathlib4#9432~~
• ~~leanprover-community/mathlib4#13060~~
• ~~leanprover-community/mathlib4#9433~~
• ~~leanprover-community/mathlib4#9435~~
• ~~leanprover-community/mathlib4#9436~~ By Dependent Issues (🤖). Happy coding!

Jun 10 '24 11:06 leanprover-community-mathlib4-bot

PR summary

Import changes

Dependency changes

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

Jun 10 '24 11:06 github-actions[bot]

Thanks and congratulations 🎉 maintainer merge

Jun 10 '24 17:06 alreadydone

🚀 Pull request has been placed on the maintainer queue by alreadydone.

Jun 10 '24 17:06 github-actions[bot]

Thanks!!!

bors merge

Jun 10 '24 19:06 riccardobrasca

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

Jun 10 '24 19:06 mathlib-bors[bot]