theorem AbelJacobi.abelJacobi_surjective (F : Type u_1) [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : Function.Surjective ⇑WeierstrassCurve.Affine.Point.toClass

Abel-Jacobi surjectivity: every divisor class in Pic⁰(W) is represented by a point of the elliptic curve W. Together with injectivity this gives the bijection W ≅ Pic⁰(W) (Thm 17.2, Lec 17).

theorem AbelJacobi.abelJacobi_bijective (F : Type u_1) [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : Function.Bijective ⇑WeierstrassCurve.Affine.Point.toClass

Abel-Jacobi bijectivity for an elliptic curve W: the map sending a point to its divisor class is a bijection W.Point ≃ Pic⁰(W) (Thm 17.2, Lec 17).

noncomputable def AbelJacobi.abelJacobiEquiv (F : Type u_1) [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : W.Point ≃+ Additive (ClassGroup W.CoordinateRing)

Abel-Jacobi as an additive equivalence: for an elliptic curve W over F, the points form an abelian group isomorphic to Pic⁰(W) = ClassGroup W.CoordinateRing.

@[reducible]

noncomputable def AbelJacobi.ellipticCurve_addCommGroup (F : Type u_1) [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : AddCommGroup W.Point

The abelian group structure on the points of an elliptic curve obtained by transport along the Abel-Jacobi equivalence with Pic⁰(W).