-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebraic_geometry/EllipticCurve/weierstrass): define Weierstrass polynomials and prove basic facts #17631
Conversation
…polynomials (#17664) + To show a monic polynomial `p` over a commutative semiring without zero divisors is irreducible, it suffices to show that `p ≠ 1` and that there doesn't exist a factorization into the product of two monic polynomials of positive degrees: `monic.irreducible_iff_nat_degree`. + If such a factorization exists, one of the polynomial must have degree less than or equal to `p.nat_degree / 2`: `monic.irreducible_iff_nat_degree'`. + To show a quadratic monic polynomial `p` is reducible, it suffices to it doesn't factor as `(X+c)(X+c')`, i.e. there don't exist `c` and `c'` that add up to the 1st coefficient and multiply up to the 0th coefficient: `not_irreducible_iff_exists_add_mul_eq_coeff`. + Define the ring homomorphism `constant_coeff` in *coeff.lean* which is analogous to [mv_polynomial.constant_coeff](https://leanprover-community.github.io/mathlib_docs/data/mv_polynomial/basic.html#mv_polynomial.constant_coeff); use it to golf and generalize `is_unit_C` and `eq_one_of_is_unit_of_monic` in *monic.lean* and various lemmas in *ring_division.lean*. + Add `monic.is_unit_iff`. + Golf some lemmas in *erase_lead.lean*. Co-authored-by: Thomas Browning <thomas.l.browning@gmail.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl> Inspired by #17631
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, LGTM! Was busy and just had a chance to review.
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…s polynomials and prove basic facts (#17631) Define the Weierstrass polynomial and its partial derivatives, as well as properties of their evaluations (the Weierstrass equation and nonsingularity). Prove that a Weierstrass curve is nonsingular at every point if its discriminant is non-zero, and its coordinate ring is an integral domain (because the associated polynomial is irreducible). Fix minor issues (rename the variable `C` with the variable `W` to avoid a clash with `polynomial.C`, and generalise `two_torsion_polynomial_disc_ne_zero`). Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Define the Weierstrass polynomial and its partial derivatives, as well as properties of their evaluations (the Weierstrass equation and nonsingularity). Prove that a Weierstrass curve is nonsingular at every point if its discriminant is non-zero, and its coordinate ring is an integral domain (because the associated polynomial is irreducible). Fix minor issues (rename the variable
C
with the variableW
to avoid a clash withpolynomial.C
, and generalisetwo_torsion_polynomial_disc_ne_zero
).Co-authored-by: Junyan Xu junyanxumath@gmail.com