feat(AlgebraicGeometry/EllipticCurve/Projective): implement group law for projective coordinates

[Multramate]

Completes the proof of the group law in projective coordinates.

---

• depends on: [Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Projective): implement equations and nonsingularity for projective coordinates #9416
• depends on: feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operation polynomials for projective coordinates #9417
• depends on: feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operations on point representatives for projective coordinates #9418
• depends on: feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operations on nonsingular rational points for projective coordinates #9420

[kbuzzard]

David you are far more likely to get this material into mathlib easily if you break it up into far smaller chunks, and write an extensive module docstring explaining what you are doing. I just envisage this PR sitting open for months otherwise.

[alreadydone]

The implementation I had in mind is to define the projective space as a subtype (or just a subset) of a quotient type (by the analogue of PointRel R) of Fin 3 → R, and define the points as a subtype of that (or just a smaller subset of the quotient type). Doesn't Fin 3 make it easier to connect to MvPolynomial? I think my proposal might be more broadly applicable and convenient, but you have more experience working on this to decide.

[alreadydone]

Sorry, it seems your implementation is pretty close to what I have in mind, just that you're using (x y z : R) rather than Fin 3 → R. But I think PointRel and general APIs (e.g. reduction) should be defined in terms of tuples indexed by an arbitrary type (Fin 3 here) to be more widely applicable.

[Multramate]

Yeah, I wrote and rewrote this about seven times and I did have Fin 3 → R originally, but here are two possible issues:

• I would have to write a Setoid instance for Fin 3 → R that is visible globally (e.g. for use in other files downstream), which might pose some problems for other people who don't want this instance (e.g. when I want the analogous thing for weighted projective space). Maybe this is a non-issue but I'm not sure.
• At the beginning I had the issue that P is not defeq to ![P.0, P.1, P.2] (whereas my P is defeq to <P.x, P.y, P.z>), and this is slightly annoying when trying to define some predicates and structures in term mode (not a problem for proofs). I have since rewritten the entire file several times so maybe this is no longer problematic.

If you think these aren't big issues, I can try making it work for Fin 3 → R again.

[alreadydone]

I would have to write a Setoid instance for Fin 3 → R that is visible globally (e.g. for use in other files downstream), which might pose some problems for other people who don't want this instance (e.g. when I want the analogous thing for weighted projective space). Maybe this is a non-issue but I'm not sure.

The usual approach is make the instSetoidPointRep a def and write attribute [local instance] when you need to activate it.

At the beginning I had the issue that P is not defeq to ![P.0, P.1, P.2] (whereas my P is defeq to <P.x, P.y, P.z>), and this is slightly annoying when trying to define some predicates and structures in term mode (not a problem for proofs). I have since rewritten the entire file several times so maybe this is no longer problematic.

I don't quite get what the problem in term mode is and would appreciate an example. And what are the "structures" that you mention? In any case, wouldn't you define predicates in terms of P 0, P 1 and P 2 the same way you define them in terms of P.x, P.y and P.z? You then need to supply a proof it's well-defined to define predicates on the quotient type, but you can do it in tactic mode.

[Multramate]

Fair enough. I don't have an example in mind because this was a while ago. Let me try this again.

[alreadydone]

Just realized: PointRel can be defined on any R-module (not just ι → R) and is actually already available as the MulAction.orbitRel of Units.instMulActionUnitsToMonoidToDivInvMonoidInstGroupUnits, so we can just define PointClass as the MulAction.orbitRel.Quotient.

For modules of the form ι → R we can show the ideal generated by the coordinates is invariant under the action, and define the projective space as the subtype where this ideal is the unit ideal. I can't find this in your code, maybe because you don't need this. (Because it's implied by the nonsingularity condition? Maybe we should redefine nonsingularity in terms of the ideal generated by the partial derivatives for compatibility with the projective space and smoothness.)

[Multramate]

I replaced PointRep with Fin 3 → R, but now there will be lots of matrix_simp's and smul_fin3's sprinkled in places.

Yes it's implied by the nonsingularity condition. Why do you need the predicates to be defined in terms of ideal generated by the coordinates or partial derivatives? Is this because your base ring is not a field?

[alreadydone]

I replaced PointRep with Fin 3 → R, but now there will be lots of matrix_simp's and smul_fin3's sprinkled in places.

Thanks! The diff of a839ab looks pretty reasonable to me (+394 -397). When I'm looking at it I realize that P 0 P 1 P 2 etc. is more obscure than the old P.x P.y P.z, and I came up with some potential tricks to use notations similar to the old ones:

We may introduce a abbrev axis := Fin 3 and use axis → R instead of Fin 3 → R. Then we define def axis.x : axis := 0, def axis.y : axis := 1 etc. so that for P : axis → R we may write P .x etc. Or maybe we can just introduce private def Fin.x : Fin 3 := 0 etc. without introducing axis. We could also introduce axis as an inductive type of three constructors x, y, and z, and the advantage would be being able to use cases rather than fin_cases. (Maybe Lean 4's cases can do fin_cases as well? Anyway I don't think this is that much an advantage.)

Yes it's implied by the nonsingularity condition. Why do you need the predicates to be defined in terms of ideal generated by the coordinates or partial derivatives? Is this because your base ring is not a field?

The condition feels more natural as it's preserved by ring homomorphisms and invariant under the action by the group of units, and I think if you define the projective points this way then E(R) maps to E(Frac R) and E(R/m) which identifies E(R) as the nonsingular points of E(Frac R) that reduces to nonsingular points of E(R/m) (for R a DVR, say). And the unit ideal condition on projective points easily reduces to that on the affine points, because of the identity $XF_X+YF_Y+ZF_Z=\text{deg }F\cdot F$ for homogeneous F means that for a point on the curve in the affine chart $Z=1$, $F_Z$ is always contained in the ideal generated by $F_X$ and $F_Y$.

[Multramate]

Would the current definitions be too troublesome for the maps you need? I would think R -> Frac R and R -> R / m are just baseChanges over algebras, and we have the corresponding baseChange on the nonsingular points.

I'm trying to give analogous definitions for weighted projective points, and I'm not sure how easy it is to rephrase everything in terms of ideals in this case, and I still need to do the same for the group law, which is why I'm hesitating.

[Multramate]

Seems like a local notation suffices if we just need it to be pretty in the file.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/Projective): implement equations and nonsingularity for projective coordinates #9416
• feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operation polynomials for projective coordinates #9417
• feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operations on point representatives for projective coordinates #9418
• feat(AlgebraicGeometry/EllipticCurve/Projective): implement group operations on nonsingular rational points for projective coordinates #9420
  By Dependent Issues (🤖). Happy coding!

[alreadydone]

Some initial comments

[alreadydone]

inline

[alreadydone]

presumably

Suggested change

	attribute [pp_dot] Point.point
	attribute [pp_dot] Point.nonsingular
	attribute [pp_dot] Point.point Point.nonsingular

[alreadydone]

capitalize (ditto for Nonsingular(Lift))

[alreadydone]

negAddXOfXNe?
(I don't care much since I won't need the projective addition formulas for the reduction homomorphism. The projective addition formulas have the same number of cases as the affine formulas, so we can just transfer the affine addition formulas through the Equiv on Points, and the projective formulas do not look more computable than the affine ones (basically you need to check the same amount of conditions).)

See my later comment: https://github.com/leanprover-community/mathlib4/pull/8485/files#r1649475618

[alreadydone]

inline

[Multramate]

Thanks for the comments. I won't be touching this PR until the Jacobian project is over, but I will keep these in mind.

[alreadydone]

I think these could be called ![W.dblX P, W.dblY P, W.dblZ P] and ![W.addX P, W.addY P, addZ P] just like the Jacobian case. In fact, I've found that you can remove a P z ^ 2 factor from the projective doubling formula to make it valid in all cases (O+O or P+P for P 2-torsion); the resulting formula is homogeneous of degree 4 rather than 6. From the projective addition formula, you can also remove a factor of P z * Q z, and the resulting formula is homogeneous of degree 6 rather than 8, and applies in the case P=-Q≠Q, but not in the cases P=O or Q=O (gives (0,0,0)). I don't think this simplifies the proof that the reduction map is a homomorphism though.

I think this is the best you can do in projective coordinates, which is not as nice as the Jacobian formulas, where both doubling and addition are weighted homogeneous of degree (8,12,4) and applies more universally without needing to single out the cases P+O and O+P.

The way to remove the factors is as follows: for Xne/add, subtract $z_1^3 F(x_2,y_2,z_2)+z_2^3 F(x_1,y_1,z_1)$ (where $F$ is W.polynomial) from addX'_of_Xne, then it becomes divisible by $z_1 z_2$. Plug this into addY'_of_Xne and add $-y_1 z_1^3 z_2 F(x_2, y_2, z_2) + y_2 z_1 z_2^3 F(x_1, y_1, z_1)$, then it also becomes divisible by $z_1 z_2$ (in fact even by its square). For the Yne/dbl, add $9x F(x,y,z)$ to addX'_of_Yne then it becomes divisible by $z$; the other factor of $z$ is added when passing to addX_of_Yne. Plug this new version of addX'_of_Yne + $(a_1^2 + 3 a_2)F(x,y,z)$ into addY'_of_Yne and subtract $z(3 a_1^2 x^2 + 9 a_1 x y + 9 y^2) P[x, y, z]$, then addY'_of_Yne becomes divisible by $z^2$.