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(AlgebraicGeometry/EllipticCurve/Jacobian): implement equations and nonsingularity for Jacobian coordinates #9432
Conversation
lemma nonsingular_zero [Nontrivial R] : W.nonsingular ![1, 1, 0] := | ||
(W.nonsingular_iff ![1, 1, 0]).mpr ⟨W.equation_zero, | ||
by simp; by_contra! h; exact one_ne_zero <| by linear_combination -h.1 - h.2.1⟩ | ||
|
||
lemma nonsingular_zero' [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : | ||
W.nonsingular ![Y ^ 2, Y ^ 3, 0] := | ||
(W.nonsingular_iff ![Y ^ 2, Y ^ 3, 0]).mpr ⟨W.equation_zero' Y, | ||
by simp [hy]; by_contra! h; exact pow_ne_zero 3 hy <| by linear_combination Y ^ 3 * h.1 - h.2.1⟩ |
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.
Some nonterminal simps here and the behavior is a bit nonpredictable; the first simp
results in ¬0 = 3 ∨ ¬1 = -1 ∨ ¬W.a₁ = 0
while the second results in ¬3 = 0 ∨ ¬Y ^ 3 = -Y ^ 3 ∨ ¬W.a₁ = 0
(the order of 3 and 0 is changed). However, if this breaks it's probably not hard to figure out what linear combination to use by inspecting the simp'd expressions. Here's a slight generalization to the second proof:
lemma nonsingular_zero [Nontrivial R] : W.nonsingular ![1, 1, 0] := | |
(W.nonsingular_iff ![1, 1, 0]).mpr ⟨W.equation_zero, | |
by simp; by_contra! h; exact one_ne_zero <| by linear_combination -h.1 - h.2.1⟩ | |
lemma nonsingular_zero' [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : | |
W.nonsingular ![Y ^ 2, Y ^ 3, 0] := | |
(W.nonsingular_iff ![Y ^ 2, Y ^ 3, 0]).mpr ⟨W.equation_zero' Y, | |
by simp [hy]; by_contra! h; exact pow_ne_zero 3 hy <| by linear_combination Y ^ 3 * h.1 - h.2.1⟩ | |
lemma nonsingular_zero [Nontrivial R] : W.nonsingular ![1, 1, 0] := | |
(W.nonsingular_iff ![1, 1, 0]).mpr ⟨W.equation_zero, | |
by simp; by_contra! h; exact one_ne_zero <| by linear_combination -h.1 - h.2.1⟩ | |
lemma nonsingular_zero' [IsReduced R] {Y : R} (hy : Y ≠ 0) : | |
W.nonsingular ![Y ^ 2, Y ^ 3, 0] := | |
(W.nonsingular_iff ![Y ^ 2, Y ^ 3, 0]).mpr ⟨W.equation_zero' Y, by | |
simp; contrapose! hy; exact IsNilpotent.eq_zero ⟨4, by linear_combination -hy.1 - Y * hy.2.1⟩⟩ |
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.
Similar to the projective file, I think we can relegate this to a future PR.
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!
Thanks! |
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Thanks! bors merge |
…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
Pull request successfully merged into master. Build succeeded: |
…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
Define a Jacobian point representative over a ring
R
as the typeFin 3 -> R
, and its equivalence classPointClass
as a quotient by the usual weighted scaling relation. Define the analogousequation
andnonsingular
predicates onFin 3 -> F
over a fieldF
, and liftnonsingular
toPointClass
. This also has minimal API (e.g. it's missing many of theequation
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