[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Weierstrass): elliptic curves with specified j-invariant #5935

acmepjz · 2023-07-16T00:29:50Z

Main changes:

Define specific Weierstrass curves, whose j-invariants should be 0, 1728, or ≠ 0 and 1728.
Prove the quantities c₄, Δ and j for them (whenever they are defined).
Define an elliptic curve from an element j in a field, whose j-invariant is equal to j.
Generalize Inhabited (EllipticCurve ℚ) to Inhabited (EllipticCurve F) for any field F (computable if F has DecidableEq).

Multramate

I've added some comments, mostly stylistic based on old conventions in the same file.

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>

acmepjz · 2023-07-18T10:32:25Z

Now I got strange error again: rw refuses to rewrite the result obtained from unitOfInvertible_val, although they look the same on the info panel.

Multramate · 2023-07-18T12:48:27Z

Now I got strange error again: rw refuses to rewrite the result obtained from unitOfInvertible_val, although they look the same on the info panel.

You will need to supply the instance argument explicitly, e.g. @unitOfInvertible _ _ _ <| invertibleNeg _.

Multramate

I finally managed to convert ofJ into term mode.

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>

… 'two_or_three_ne_zero'

FIXME: This is unfortunately noncomputable

In the general case, by adding 'Classical' and 'noncomputable', it implies a noncomputable 'DecidableEq'

acmepjz · 2023-07-23T19:27:31Z

Is it a good idea to remove remaining noncomputable in this file, as many as possible, by adding DecidableEq instance (possibly in another PR)? This has a disadvantage then it introduces classical if the relevant ring does not have DecidableEq.

Multramate · 2023-07-24T16:39:27Z

Is it a good idea to remove remaining noncomputable in this file, as many as possible, by adding DecidableEq instance (possibly in another PR)? This has a disadvantage then it introduces classical if the relevant ring does not have DecidableEq.

I don't know anything about this. All I know for the inhabited instance is that we should have 37 instead of 42. 😉

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>

…me.Lemmas'

riccardobrasca · 2023-08-01T13:22:20Z

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

+    by rw [h1728, show (1728 : F) = 2 * 864 by norm_num1, h, zero_mul]
+  else @ofJ' _ _ j (invertibleOfNonzero h0) (invertibleOfNonzero <| sub_ne_zero_of_ne h1728)
+
+lemma ofJ_0_of_three_ne_zero (h3 : (3 : F) ≠ 0) : ofJ 0 = @ofJ0 _ _ (invertibleOfNonzero h3) := by


What about using NeZero instead of h3? Similarly elsewhere.

Sounds good. I'll try later.

# Conflicts: # Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

acmepjz · 2023-08-01T19:27:25Z

@riccardobrasca I tried NeZero but I think the resulting code looks weird. We don't have NeZero -> Invertible automatic conversion even if it's a field. Also we don't have EqZero. So now the code is a mix of typeclass and explicit assumptions.

riccardobrasca · 2023-08-03T09:03:04Z

@riccardobrasca I tried NeZero but I think the resulting code looks weird. We don't have NeZero -> Invertible automatic conversion even if it's a field. Also we don't have EqZero. So now the code is a mix of typeclass and explicit assumptions.

OK, no problem if it becomes a mess. Thanks!

bors merge

bors · 2023-08-03T09:03:08Z

Already running a review

…th specified j-invariant (#5935) Main changes: - [x] Define specific Weierstrass curves, whose j-invariants should be 0, 1728, or ≠ 0 and 1728. - [x] Prove the quantities c₄, Δ and j for them (whenever they are defined). - [x] Define an elliptic curve from an element j in a field, whose j-invariant is equal to j. - [x] Generalize `Inhabited (EllipticCurve ℚ)` to `Inhabited (EllipticCurve F)` for any field `F` (computable if `F` has `DecidableEq`).

bors · 2023-08-03T10:45:05Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

…th specified j-invariant (#5935) Main changes: - [x] Define specific Weierstrass curves, whose j-invariants should be 0, 1728, or ≠ 0 and 1728. - [x] Prove the quantities c₄, Δ and j for them (whenever they are defined). - [x] Define an elliptic curve from an element j in a field, whose j-invariant is equal to j. - [x] Generalize `Inhabited (EllipticCurve ℚ)` to `Inhabited (EllipticCurve F)` for any field `F` (computable if `F` has `DecidableEq`).

acmepjz added 2 commits July 16, 2023 08:25

added elliptic curves with specified j-invariant (WIP)

400b02d

fixed the type mismatch bug

739d4d4

acmepjz marked this pull request as ready for review July 16, 2023 10:45

'Classical' is not necessary

3081903

Multramate reviewed Jul 16, 2023

View reviewed changes

acmepjz and others added 9 commits July 17, 2023 16:09

Apply suggestions from code review

4301fe2

Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>

Update Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

13bdafc

Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>

added spaces to j-1728

69557bf

merge different sections (?)

14000c2

try again

156aba4

rename 'JInvariant' to 'J' and added document strings

b8e27c3

removed some sections

5ecc70d

makes 'ofJ0' simpler

468503a

makes another two simpler, but it does not work yet

95ae5c7

Multramate reviewed Jul 18, 2023

View reviewed changes

acmepjz and others added 6 commits July 19, 2023 08:12

Apply suggestions from code review

f69e558

Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>

add missing lemmas

b44292c

Merge branch 'master' into acmepjz_ec_exists_j

e692f41

add 'ne_zero_or_ne_zero_of_nat_gcd_eq_one' which slightly generalizes…

cb3adae

… 'two_or_three_ne_zero'

'EllipticCurve F' is inhabited for any field 'F', not only rational

fd0ba67

FIXME: This is unfortunately noncomputable

get rid of 'Classical' and 'noncomputable' by adding 'DecidableEq'

99b50c1

In the general case, by adding 'Classical' and 'noncomputable', it implies a noncomputable 'DecidableEq'

42 -> 37

6757b5d

Multramate added awaiting-review The author would like community review of the PR t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebraic-geometry Algebraic geometry labels Jul 26, 2023

Merge branch 'master' into acmepjz_ec_exists_j

26b7ce5

Multramate approved these changes Jul 29, 2023

View reviewed changes

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean Outdated Show resolved Hide resolved

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean Outdated Show resolved Hide resolved

Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean Outdated Show resolved Hide resolved

acmepjz and others added 4 commits July 30, 2023 00:46

Apply suggestions from code review

15b26c5

Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>

Merge branch 'master' into acmepjz_ec_exists_j

309ee4a

move 'ne_zero_or_ne_zero_of_nat_coprime' to 'Mathlib.RingTheory.Copri…

d97c4b3

…me.Lemmas'

slightly refactor

c35d7b6

riccardobrasca reviewed Aug 1, 2023

View reviewed changes

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 1, 2023

Merge branch 'master' into acmepjz_ec_exists_j

58defff

# Conflicts: # Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Aug 1, 2023

use NeZero instead; but the code feels weird

5cafbab

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Aug 3, 2023

bors bot changed the title ~~feat(AlgebraicGeometry/EllipticCurve/Weierstrass): elliptic curves with specified j-invariant~~ [Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Weierstrass): elliptic curves with specified j-invariant Aug 3, 2023

bors bot closed this Aug 3, 2023

bors bot deleted the acmepjz_ec_exists_j branch August 3, 2023 10:45

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Weierstrass): elliptic curves with specified j-invariant #5935

[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Weierstrass): elliptic curves with specified j-invariant #5935

acmepjz commented Jul 16, 2023 •

edited

Loading

Multramate left a comment

acmepjz commented Jul 18, 2023

Multramate commented Jul 18, 2023

Multramate left a comment

acmepjz commented Jul 23, 2023

Multramate commented Jul 24, 2023

riccardobrasca Aug 1, 2023

acmepjz Aug 1, 2023

acmepjz commented Aug 1, 2023

riccardobrasca commented Aug 3, 2023

bors bot commented Aug 3, 2023

bors bot commented Aug 3, 2023

[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Weierstrass): elliptic curves with specified j-invariant #5935

[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Weierstrass): elliptic curves with specified j-invariant #5935

Conversation

acmepjz commented Jul 16, 2023 • edited Loading

Multramate left a comment

Choose a reason for hiding this comment

acmepjz commented Jul 18, 2023

Multramate commented Jul 18, 2023

Multramate left a comment

Choose a reason for hiding this comment

acmepjz commented Jul 23, 2023

Multramate commented Jul 24, 2023

riccardobrasca Aug 1, 2023

Choose a reason for hiding this comment

acmepjz Aug 1, 2023

Choose a reason for hiding this comment

acmepjz commented Aug 1, 2023

riccardobrasca commented Aug 3, 2023

bors bot commented Aug 3, 2023

bors bot commented Aug 3, 2023

acmepjz commented Jul 16, 2023 •

edited

Loading