[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): add maps for division polynomials

[Multramate]

---

• depends on: [Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): define division polynomials #6703
• depends on: [Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Affine): add further map lemmas #13356

[alreadydone]

Thanks 🎉
This is now good for merging again.

[github-actions]

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

[jcommelin]

Does it make sense to put this in a new file? Because the current import adds 300 new transitive imports. Or do you think that everything importing .Basic will also want access to the new results from this PR anyways?

[Multramate]

Does it make sense to put this in a new file? Because the current import adds 300 new transitive imports. Or do you think that everything importing .Basic will also want access to the new results from this PR anyways?

Very understandable. I do think that users of \Psi and \Phi should have access to their equivalence with \psi and \phi in the coordinate ring, because that's the original motivation for having separate definitions. This only requires the definition of the coordinate ring and some basic properties, hence only requires importing AdjoinRoot and Norm. Unfortunately the file defining the coordinate ring is interlaced with the proof of the group law that imports ClassGroup, which presumably is the majority of the 300+ transitive imports. How about this: let's merge this PR, and I'll open another PR immediately that splits off the stuff on the coordinate ring into another file, and this file can just import that new file.

[alreadydone]

The central result about division polynomials is the formula for zsmul on the group of rational points in terms of division polynomials, and the group structure already require CoordinateRing (AdjoinRoot), ClassGroup and Norm, so I don't think it makes much sense to avoid them.

[Multramate]

Yes, but ZSMul.lean or Group.lean will be a different file from Basic.lean. Maybe there are uses of division polynomials without needing the fact that the points form a group, e.g. if you just need an explicit duplication/triplication formula?

I think it's probably good to split off a file just for the coordinate ring anyway - this can include all the API for the universal elliptic curve, the evaluation and specialisation maps, and whatever else that are universal constructions.

Now that I think of it, we don't actually need the two definitions to agree until we actually compute the structure of the n-torsion. Maybe I'll leave the lemmas here for now, and the move it out eventually once I get to that.

[alreadydone]

just need an explicit duplication/triplication formula

I think my proof of the duplication formula (in terms of division polynomials) doesn't use the group axioms (can be extracted from these two lemmas), but the triplication formula (which is not established until the final theorem) uses the group structure.

[alreadydone]

It seems our consensus is to merge this PR first, so let's do that and worry about splitting later? If you put your proposed splitting in some branch I can check whether it's reasonable ...

[alreadydone]

In fact, I think it's pretty rare that people would want to talk about elliptic curves without knowing the rational points form a group. Do you have such examples in mind?

[YaelDillies]

I tend to agree that the split can be done later, if at all

[Multramate]

In fact, I think it's pretty rare that people would want to talk about elliptic curves without knowing the rational points form a group. Do you have such examples in mind?

Not specifically the theory of division polynomials, but my primary example would be moduli problems (e.g. the moduli stack of genus one curves, or just modular curves X/X_0/X_1), where the group law is not relevant? Obviously this is very far away and proving any useful theorems about moduli spaces would require some form of Riemann-Roch, in which case the group law is pretty much automatic, but maybe there's a nice description of the Weierstrass coefficients in terms of the moduli space.

Another argument for avoiding the import could be if the user prefers to write a different group law (e.g. the one induced by complex uniformisation), which might have properties easier to work with, but that's probably a weak argument.

[alreadydone]

Well, the modular curves seem pretty closely connected to the group structure:

You might be able to define modular curves through their own equations but as soon as you connect them to elliptic curves you'd be talking about torsion points.

[Vierkantor]

The code looks good to me, and the consensus seems to be that the imports are okay or can be split later on. So let's get this merged.

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style