David Kurniadi Angdinata

refactor(algebraic_geometry/projective_spectrum/topology): refactor projective_spectrum def into structure

1

- [x] depends on: #16920 [refactor height one spectrum] - [ ] depends on: #16930 [refactor prime spectrum] --- [](https://gitpod.io/from-referrer/)

refactor(algebraic_geometry/prime_spectrum/basic): refactor prime_spectrum def into structure

1

- [x] depends on: #16920 [refactor height one spectrum] --- [](https://gitpod.io/from-referrer/)

feat(algebraic_geometry/prime_spectrum/basic): intersection of localisations

5

- [x] depends on: #16905 [define maximal spectrum] - [x] depends on: #16920 [refactor height one spectrum] --- [](https://gitpod.io/from-referrer/)

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial): define division polynomials

2

--- - [x] depends on: #10814 [](https://gitpod.io/from-referrer/)

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

6

Completes the proof of the group law in Jacobian coordinates, analogously to #8485 --- - [x] depends on: #9432 - [ ] depends on: #9433 - [ ] depends on:...

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on nonsingular rational points for Jacobian coordinates

1

Define a addition-preserving bijection `toAffine_addEquiv` with the affine case to prove `Point` is an abelian group. This is the fourth in a series of four PRs leading to #9405 and...

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on point representatives for Jacobian coordinates

1

Define the analogous secant-and-tangent negation `neg` and addition `add` on `PointRep` over `F`, and lift them to `PointClass`. Define `Point` as a `PointClass` that is nonsingular. Prove in `neg_equiv` and...

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operation polynomials for Jacobian coordinates

1

Define auxiliary polynomials for the secant-and-tangent negation `neg` and addition `add` on `Fin 3 -> F`. Note that the group operations are defined from scratch instead of pulling back the...

--- [](https://gitpod.io/from-referrer/)

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial): compute degrees of division polynomials

2

--- - [x] depends on: #10814 - [ ] depends on: #10843 [](https://gitpod.io/from-referrer/)