@[implicit_reducible]

instance elliptic_curve_group_structure {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : AddCommGroup W.Point

The set of points on an affine elliptic curve forms an abelian group under the chord-tangent law: this is the analytic / classical group law on E(F).

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

The Abel-Jacobi map Point.toClass from points on the elliptic curve to the class group of the coordinate ring is surjective: every divisor class is represented by a point (Cor 21, Lec 14/15).

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

Cor 21: the Abel-Jacobi map is a bijection, identifying the group of points on an elliptic curve with the class group of its coordinate ring.