Skip to content
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.

Sign up for GitHub

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

Jump to bottom

feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types #14627

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

feat(AlgebraicGeometry/EllipticCurve/Affine): add equivalences between points and explicit WithZero types #14627

wants to merge 7 commits into from
+159 −52

Conversation

Multramate
Copy link
Collaborator

Open in Gitpod

@Multramate Multramate added awaiting-CI t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-algebraic-geometry Algebraic geometry labels Jul 10, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 10, 2024 •
edited
Loading

PR summary d9f0583dc5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Point.mk
+ equation_zero_iff_nonsingular_zero
+ instance : Add W.Point
+ instance : AddZeroClass W.Point
+ pointEquivEquation
+ pointEquivEquationSubtype
+ pointEquivEquationSubtype_some
+ pointEquivEquationSubtype_symm_none
+ pointEquivEquationSubtype_symm_some
+ pointEquivEquationSubtype_zero
+ pointEquivEquation_some
+ pointEquivEquation_symm_none
+ pointEquivEquation_symm_some
+ pointEquivEquation_zero
+ pointEquivNonsingular
+ pointEquivNonsingularSubtype
+ pointEquivNonsingularSubtype_some
+ pointEquivNonsingularSubtype_symm_none
+ pointEquivNonsingularSubtype_symm_some
+ pointEquivNonsingularSubtype_zero
+ pointEquivNonsingular_some
+ pointEquivNonsingular_symm_none
+ pointEquivNonsingular_symm_some
+ pointEquivNonsingular_zero
++ equation_iff_nonsingular
- instAddPoint
- instAddZeroClassPoint
- mk
- nonsingular
- nonsingular_of_Δ_ne_zero
- nonsingular_zero_of_Δ_ne_zero

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

The doc-module for script/declarations_diff.sh contains some details about this script.

@Multramate
Copy link
Collaborator Author

These equivalences will be useful to show the equivalence between the current inductive definition of A-points and the scheme-theoretic definition of A-points as morphisms in the category of schemes over Spec R, (see e.g. #14130 or #14167), but also to have an explicit description of certain subgroups (e.g. the n-torsion subgroup in terms of division polynomials).

@erdOne erdOne requested a review from alreadydone July 18, 2024 08:22
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 19, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 19, 2024
@Multramate Multramate mentioned this pull request Jul 19, 2024
Open
1 task
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 9, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 23, 2024
Ruben-VandeVelde
Ruben-VandeVelde reviewed Sep 9, 2024
View reviewed changes
Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@@ -274,18 +273,19 @@ lemma nonsingular_iff_variableChange (x y : R) :
simp only [variableChange]
congr! 3 <;> ring1

lemma nonsingular_zero_of_Δ_ne_zero (h : W.Equation 0 0) (hΔ : W.Δ ≠ 0) : W.Nonsingular 0 0 := by
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please leave a (deprecated) alias with the existing name

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
/-- A Weierstrass curve is nonsingular at every point if its discriminant is non-zero. -/
lemma nonsingular_of_Δ_ne_zero {x y : R} (h : W.Equation x y) (hΔ : W.Δ ≠ 0) : W.Nonsingular x y :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And this one as well

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
nonsingular_zero_of_Δ_ne_zero _ ((W.equation_iff_variableChange x y).mp h) <| by
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]

lemma equation_iff_nonsingular {x y : R} (hΔ : W.Δ ≠ 0) : W.Equation x y ↔ W.Nonsingular x y := by
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there any reason to use equation_zero_iff_nonsingular_zero once this one exists? If not, mark the former as private or even inline it into this lemma

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
Comment on lines +288 to 289
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]
end Nonsingular
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]
end Nonsingular
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]
end Nonsingular

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@@ -637,7 +696,7 @@ lemma neg_some {x y : R} (h : W.Nonsingular x y) : -some h = some (nonsingular_n
rfl

instance : InvolutiveNeg W.Point :=
⟨by rintro (_ | _) <;> simp [zero_def]; ring1⟩
⟨by rintro (_ | _); rfl; simp only [neg_some, negY_negY]⟩
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Focusing dot for each subgoal, please

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
Comment on lines -655 to +714
noncomputable instance instAddPoint : Add W.Point :=
noncomputable instance : Add W.Point :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Any reason?

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

lemma nonsingular [Nontrivial R] {x y : R} (h : E.toAffine.Equation x y) :
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did this one go anywhere?

@Ruben-VandeVelde Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes label Sep 9, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

@alreadydone alreadydone Awaiting requested review from alreadydone

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebraic-geometry Algebraic geometry t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@Multramate @Ruben-VandeVelde @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot