[Merged by Bors] - feat(EllipticCurve): lemmas in Jacobian coordinates #13846
Conversation
alreadydone
added
awaiting-review
awaiting-CI
t-algebraic-geometry
PR summary 5dc441b533Import changesDependency changes
|
Co-authored-by: David Kurniadi Angdinata <[email protected]>
…f other simp lemmas
alreadydone
force-pushed
the
EllCurve/Jacobian_lemmas
branch
from
d8a9c59 to
4f8e234
Compare
This reverts commit 1a5e80a but do not restore @[simp] attributes
alreadydone
force-pushed
the
EllCurve/Jacobian_lemmas
branch
from
4f8e234 to
36f1e0a
Compare
| lemma nonsingular_iff_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) : | ||
| W.Nonsingular P ↔ W.Equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0) := by | ||
| rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz, | ||
| ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 4 hPz, | ||
| ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 3 hPz] |
There was a problem hiding this comment.
Can you remind me where you need this?
There was a problem hiding this comment.
No I don't need this, but I think it's an interesting result, and it can be generalized to arbitrary comm. rings assuming P z is not a zero divisor, because in analogy to polynomial_relation in the projective API, here we have
6 * eval P W.polynomial = 2 * P x * eval P W.polynomialX + 3 * P y * eval P W.polynomialY + P z * eval P W.polynomialZ
due to weighted homogeneity, which you use with P z = 1 in nonsingular_some.
There was a problem hiding this comment.
Ah sure, can you generalise it to that context then, if it's not too difficult?
There was a problem hiding this comment.
I have it ready here but I prefer to merge this first. It's another +40 -14 on top of this.
By the way I think a more meaningful definition of Nonsingular is that the three derivatives generate the unit ideal. In order to get rid of the third derivative, the sufficient condition is IsUnit (P z) rather than P z ∈ R⁰. I'm not sure whether either of these two forms of the lemma will ever be used though.
| lemma comp_fin3 {S} (f : R → S) (X Y Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z] := by | ||
| ext i; fin_cases i <;> rfl | ||
| lemma comp_fin3 {S} (f : R → S) (X Y Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z] := | ||
| (FinVec.map_eq _ _).symm |
There was a problem hiding this comment.
Untested:
| (FinVec.map_eq _ _).symm | |
| (FinVec.map_eq ..).symm |
There was a problem hiding this comment.
Since we already have FinVec.map_eq, do we still need comp_fin3? Otherwise, should this be comp_fin3_ext, and does it make sense to have an analogous comp_fin3 for P : Fin 3 -> R?
There was a problem hiding this comment.
As I commented, it can't be used to rewrite to the desired form directly.
Co-authored-by: David Kurniadi Angdinata <[email protected]>
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
+ `equiv_iff_eq_of_Z_eq`: if a point has two representations in Jacobian coordinates with the same, nonzero Z-coordinate, then the two representations are equal. + `nonsingular_iff_of_Z_ne_zero`: a lemma deleted in an earlier PR for no reason, now restored. + `addXYZ_self`: if the addition (not doubling) formula is applied to a point representative and itself, the result is (0,0,0). + `addXYZ_neg`: the addition formula applied to a point representative and its negation yields a representative of the point at infinity. + two trivial lemmas `fromAffine_ne_zero` and `comp_fin3`. + a series of `map` lemmas showing the addition and doubling formulas in Jacobian coordinates commute with ring homomorphisms. Co-authored-by: Junyan Xu <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
+ `equiv_iff_eq_of_Z_eq`: if a point has two representations in Jacobian coordinates with the same, nonzero Z-coordinate, then the two representations are equal. + `nonsingular_iff_of_Z_ne_zero`: a lemma deleted in an earlier PR for no reason, now restored. + `addXYZ_self`: if the addition (not doubling) formula is applied to a point representative and itself, the result is (0,0,0). + `addXYZ_neg`: the addition formula applied to a point representative and its negation yields a representative of the point at infinity. + two trivial lemmas `fromAffine_ne_zero` and `comp_fin3`. + a series of `map` lemmas showing the addition and doubling formulas in Jacobian coordinates commute with ring homomorphisms. Co-authored-by: Junyan Xu <[email protected]>
+ `equiv_iff_eq_of_Z_eq`: if a point has two representations in Jacobian coordinates with the same, nonzero Z-coordinate, then the two representations are equal. + `nonsingular_iff_of_Z_ne_zero`: a lemma deleted in an earlier PR for no reason, now restored. + `addXYZ_self`: if the addition (not doubling) formula is applied to a point representative and itself, the result is (0,0,0). + `addXYZ_neg`: the addition formula applied to a point representative and its negation yields a representative of the point at infinity. + two trivial lemmas `fromAffine_ne_zero` and `comp_fin3`. + a series of `map` lemmas showing the addition and doubling formulas in Jacobian coordinates commute with ring homomorphisms. Co-authored-by: Junyan Xu <[email protected]>
equiv_iff_eq_of_Z_eq: if a point has two representations in Jacobian coordinates with the same, nonzero Z-coordinate, then the two representations are equal.nonsingular_iff_of_Z_ne_zero: a lemma deleted in an earlier PR for no reason, now restored.addXYZ_self: if the addition (not doubling) formula is applied to a point representative and itself, the result is (0,0,0).addXYZ_neg: the addition formula applied to a point representative and its negation yields a representative of the point at infinity.two trivial lemmas
fromAffine_ne_zeroandcomp_fin3.a series of
maplemmas showing the addition and doubling formulas in Jacobian coordinates commute with ring homomorphisms.