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

[Multramate]

---

• depends on: [Merged by Bors] - feat(NumberTheory/EllipticDivisibilitySequence): expose the auxiliary sequence #10814

[alreadydone]

Mostly LGTM, just a few comments

[alreadydone]

Better write this as $\tfrac{1}{2} \cdot (\psi_{2n}/\psi_n - \psi_n(a_1\phi_n + a_3\psi_n^2))$ (you're missing an ending )), and explain that how $\psi_{2n}/\psi_n$ is well-defined using preNormEDS (you can add a link to my complEDS).
Also explain that division by 2 is not possible in char 2, so either we need to divide in the universal ring over ℤ, or define $\omega$ another way (you can add a link to my definition).

I think it makes sense to merge the definition part of my DivisionPolynomial.lean with this PR, and maybe call the file DivisionPolynomial/Defs.lean, but then you'll need to wait for my #13057. The proof of the smul formula can be put in a standalone file called DivisionPolynomial/Group.lean (or ZSMul.lean ??). The degree computations can be another file Degree.lean.

[Multramate]

I'll fix the definition and add a short note explaining the issue with division by 2. I think it's a great idea to have multiple files since they're getting quite long. I'll propagate this to my downstream PRs.

I think we don't want to define $\omega$ in this PR (presumably that's what you mean by including #13057 since it's now broken to a few smaller PRs), because that is massive on its own.

[Multramate]

I added a very short description of how to define $\omega$ mathematically at the module docstrings. The actual implementation details under Implementation Notes we can add when we actually PR the definition of $\omega$.

[github-actions]

PR summary

Import changes

No significant changes to the import graph

---

Declarations diff

+ C_Ψ₂Sq_eq
+ as
+ in
+ preΨ
+ preΨ'
+ preΨ'_even
+ preΨ'_four
+ preΨ'_odd
+ preΨ'_one
+ preΨ'_three
+ preΨ'_two
+ preΨ'_zero
+ preΨ_even
+ preΨ_four
+ preΨ_neg
+ preΨ_odd
+ preΨ_ofNat
+ preΨ_one
+ preΨ_three
+ preΨ_two
+ preΨ_zero
+ preΨ₄
+ Φ
+ Φ_four
+ Φ_neg
+ Φ_ofNat
+ Φ_one
+ Φ_three
+ Φ_two
+ Φ_zero
+ Ψ
+ ΨSq
+ ΨSq_even
+ ΨSq_four
+ ΨSq_neg
+ ΨSq_odd
+ ΨSq_ofNat
+ ΨSq_one
+ ΨSq_three
+ ΨSq_two
+ ΨSq_zero
+ Ψ_even
+ Ψ_four
+ Ψ_neg
+ Ψ_odd
+ Ψ_ofNat
+ Ψ_one
+ Ψ_three
+ Ψ_two
+ Ψ_zero
+ Ψ₂Sq
+ Ψ₂Sq_eq
+ Ψ₃
+ φ
+ φ_four
+ φ_neg
+ φ_one
+ φ_three
+ φ_two
+ φ_zero
+ ψ
+ ψ_even
+ ψ_four
+ ψ_neg
+ ψ_odd
+ ψ_one
+ ψ_three
+ ψ_two
+ ψ_zero
+ ψ₂

You can run this locally as follows

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

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

[Multramate]

I only moved the files into a subdirectory in latest commit, while the changes reflecting the suggestions are in the previous commit. Note that there seems to be a weird bug with neg lemmas not recognising the negation in R[X][Y] in lines 429 and 430 without supplying the type.

[alreadydone]

I think it would be nice to include the proofs that the uppercase and lowercase $\phi$ and $\psi$ are congruent modulo W.polynomial. I think the useful statement is that there image under CoordinateRing.mk are equal. (Since evalEval at a point satisfying Equation factors through CoordinateRing.mk, the evalEval of these congruent polynomials are also equal.)

[Multramate]

Don't we need the map lemmas for that? I think I started #13399 pretty much immediately after I realised this. I suggest keeping the PR as it is and continue there.

[alreadydone]

Thanks 🎉
maintainer merge

[github-actions]

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

[riccardobrasca]

This is great, thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[alreadydone]

These two lines are broken in the documentation and I'm not sure why.

[Multramate]

Seems like it's an issue with _ being both part of markdown and LaTeX, see e.g. here.