Skip to content

feat(AlgebraicGeometry/EllipticCurve): add notation and pretty printer for points#36334

Open
Multramate wants to merge 1 commit intoleanprover-community:masterfrom
Multramate:Point.delab
Open

feat(AlgebraicGeometry/EllipticCurve): add notation and pretty printer for points#36334
Multramate wants to merge 1 commit intoleanprover-community:masterfrom
Multramate:Point.delab

Conversation

@Multramate
Copy link
Copy Markdown
Collaborator

@Multramate Multramate commented Mar 7, 2026

Co-authored-by: Kenny Lau [email protected]

Open in Gitpod

@Multramate Multramate requested a review from kckennylau March 7, 2026 20:24
@Multramate Multramate added the t-algebraic-geometry Algebraic geometry label Mar 7, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 7, 2026

PR summary bf66be1a70

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@Multramate
Copy link
Copy Markdown
Collaborator Author

Multramate commented Mar 7, 2026

The notation for affine points is pretty, but I don't have a good idea what to do for Jacobian/projective points. Ideally a point on W created from a representative [X:Y:Z] should be pretty printed as W(X:Y:Z), but since it's actually an equivalence class we'd have to choose one representative somehow? Any ideas?

@Multramate Multramate requested a review from CBirkbeck March 7, 2026 21:13
CBirkbeck
CBirkbeck reviewed Mar 9, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@CBirkbeck CBirkbeck left a comment

Choose a reason for hiding this comment

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

I think this is something we definitely want, but reviewing the code is a bit above my pay grade. But it LGTM! if that helps

@CBirkbeck CBirkbeck requested a review from riccardobrasca March 9, 2026 18:42
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Mar 9, 2026

@erdOne can you have a look? About elliptic curves I usually trust @Multramate, but it's maybe a good idea to have a look by someone else.

@Multramate
Copy link
Copy Markdown
Collaborator Author

Multramate commented Mar 9, 2026

(You should definitely not trust me because I don't trust myself on this one!)

@erdOne
Copy link
Copy Markdown
Member

erdOne commented Mar 10, 2026 •
edited
Loading

Can you add a test file for this? Thanks.
(See MathlibTest/Delab/Scheme.lean for an example; but you should test the elaborators as well)

@erdOne
Copy link
Copy Markdown
Member

erdOne commented Mar 10, 2026

Frankly, this is the very first thing I did when I tried to work with elliptic curves in mathlib, though I never came around PRing it. So I totally agree that such a notation is the reasonable thing to do.

erdOne
erdOne reviewed Mar 10, 2026
View reviewed changes
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean
/-- The notation for a nonsingular affine point `(x, y)` on a Weierstrass curve `W` over a ring
whose numerical expressions can be normalised with `norm_num`. -/
scoped notation:max W "⟮" x "," y "⟯" =>
Point.some (W' := W) x y <| by norm_num [nonsingular_iff, equation_iff]
Copy link
Copy Markdown
Member

@erdOne erdOne Mar 10, 2026

Choose a reason for hiding this comment

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

I wonder if we want notation like W⟮O⟯ for Point.zero or if we are happy with the inconsistence of notation.

Copy link
Copy Markdown
Collaborator Author

@Multramate Multramate Mar 10, 2026

Choose a reason for hiding this comment

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

This is a good idea and I am happy to add it.

@Multramate
Copy link
Copy Markdown
Collaborator Author

Multramate commented Mar 10, 2026

Can you add a test file for this? Thanks.

(See MathlibTest/Delab/Scheme.lean for an example; but you should test the elaborators as well)

I can do this; the infoview don't show properly for #eval unfortunately --- any ideas?

@erdOne
Copy link
Copy Markdown
Member

erdOne commented Mar 11, 2026 •
edited
Loading

the infoview don't show properly for #eval unfortunately

What do you mean by this? Does #eval and the infoview show different things? That's unfortunate.

@Multramate
Copy link
Copy Markdown
Collaborator Author

Multramate commented Mar 11, 2026 •
edited
Loading

the infoview don't show properly for #eval unfortunately

What do you mean by this? Does #eval and the infoview show different things? That's unfortunate.

Yes:

abbrev E : Affine ℚ := ⟨0, 0, 0, 0, 1⟩
#check E⟮0, -1⟯ -- shows E⟮0,-1⟯ : E.Point in the infoview
#eval E⟮0, -1⟯ -- shows WeierstrassCurve.Affine.Point.some 0 -1 _ in the infoview
#reduce E⟮0, -1⟯ -- shows E⟮{ num := Int.ofNat 0, den_nz := instInhabitedRat._proof_1, reduced := ⋯ },{ num := Int.negSucc 0, den_nz := ⋯, reduced := ⋯ }⟯ in the infoview

I feel like this is a solvable problem but I don't know how to solve it.

@joelriou joelriou added the t-meta Tactics, attributes or user commands label Mar 18, 2026
@dagurtomas dagurtomas removed their assignment Mar 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

@kckennylau kckennylau Awaiting requested review from kckennylau

@riccardobrasca riccardobrasca Awaiting requested review from riccardobrasca

+1 more reviewer

@CBirkbeck CBirkbeck CBirkbeck left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@kim-em kim-em

Labels

t-algebraic-geometry Algebraic geometry t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@Multramate @riccardobrasca @erdOne @CBirkbeck @kim-em @dagurtomas @joelriou