Pic⁰ of the projective model of an elliptic curve

Let W be an elliptic Weierstrass curve over a field K and let E = projModel W be its projective model, a smooth proper curve over K. This file identifies the group of points W.toAffine.Point of Mathlib, with its chord-and-tangent group law, with the degree-zero part Pic⁰ E of the Picard group of E, the group of isomorphism classes of line bundles of degree zero under tensor product (LineBundleClass.picZero).

The identification is assembled from three isomorphisms of groups:

• the points of W are the degree-zero divisor classes Cl⁰(K(W)) of the function field of the affine equation, a point P going to the class of (P) - (O) (WeierstrassCurve.Affine.pointEquivDegreeZeroDivisorClass);
• the function field of E is K(W) (WeierstrassCurve.projModelFunctionFieldEquiv), and this isomorphism respects the constants, so it identifies Cl⁰(K(E)) with Cl⁰(K(W)) (Divisor.degreeZeroClassGroupEquivOfRingEquiv);
• on a proper curve, Pic⁰ E ≅ Cl⁰(K(E)) (SchemeWeilDivisor.picZeroAddEquivDegreeZeroClassGroup).

The codimension-one points of E are identified with the places of K(W) in TauCeti.AlgebraicGeometry.EllipticCurve.Scheme.Place (WeierstrassCurve.projModelCodimensionOnePointEquivPlace). Through this identification the isomorphism sends an affine point P to the class of the line bundle 𝒪_E(x_P - x_O), where x_P and x_O are the points of E corresponding to the place of P and to the place at infinity (WeierstrassCurve.coe_pointAddEquivPicZero_some).

Main declarations

• WeierstrassCurve.projModelPicZeroAddEquiv: Pic⁰ (projModel W) ≃+ Cl⁰(K(W));
• WeierstrassCurve.pointAddEquivPicZero: W.toAffine.Point ≃+ Pic⁰ (projModel W).

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., GTM 106, Springer, 2009, Proposition III.3.4.
• R. Hartshorne, Algebraic Geometry, Chapter II, Section 6, and Chapter IV, Section 4.

instance WeierstrassCurve.finiteDimensional_cohomology_one_projModel {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : FiniteDimensional K (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial W.projModel).obj 1)

The first cohomology of the structure sheaf of the projective model of an elliptic curve is finite-dimensional.

Pic⁰ of the projective model

noncomputable def WeierstrassCurve.projModelPicZeroAddEquiv {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] : ↥(TauCeti.AlgebraicGeometry.LineBundleClass.picZero K W.projModel) ≃+ ↥(TauCeti.Divisor.degreeClass ⋯).ker

Pic⁰ of the projective model is the degree-zero divisor class group of K(W). It is the composite of Pic⁰ E ≅ Cl⁰(K(E)) with the identification of K(E) with K(W).

theorem WeierstrassCurve.coe_projModelPicZeroAddEquiv_symm_apply {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] {c : ↥(TauCeti.Divisor.degreeClass ⋯).ker} {E : TauCeti.Divisor K W.toAffine.FunctionField} (hc : ↑c = (TauCeti.Place.orderSystem ⋯).divisorClass E) : ↑(W.projModelPicZeroAddEquiv.symm c) = Additive.ofMul (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass ⋯ ((Finsupp.domCongr W.projModelCodimensionOnePointEquivPlace.symm) E))

The inverse of projModelPicZeroAddEquiv sends the class of a degree-zero divisor E of K(W) to the class of the line bundle 𝒪(D) on projModel W, where D is the divisor on projModel W with the same coefficients at corresponding points and places.

noncomputable def WeierstrassCurve.pointAddEquivPicZero {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] : W.toAffine.Point ≃+ ↥(TauCeti.AlgebraicGeometry.LineBundleClass.picZero K W.projModel)

The points of an elliptic curve form Pic⁰ of its projective model. For an elliptic curve W over a field K, the group W.toAffine.Point of Mathlib, with its chord-and-tangent group law, is isomorphic to the group Pic⁰ (projModel W) of degree-zero line bundles on the projective model. The point at infinity goes to the trivial bundle, and an affine point P to the class of 𝒪(x_P - x_O) (coe_pointAddEquivPicZero_some).

theorem WeierstrassCurve.coe_pointAddEquivPicZero_some {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] [DecidableEq K] {x y : K} (h : W.toAffine.Nonsingular x y) : ↑(W.pointAddEquivPicZero (Affine.Point.some x y h)) = Additive.ofMul (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.toLineBundleClass ⋯ (TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (W.projModelCodimensionOnePointEquivPlace.symm (TauCeti.Place.ofPrime K W.toAffine.FunctionField (Affine.CoordinateRing.pointPlace ⋯))) - TauCeti.AlgebraicGeometry.WeilDivisor.ofPoint (W.projModelCodimensionOnePointEquivPlace.symm (TauCeti.Place.infinity W.toAffine))))

An affine point goes to the class of 𝒪(x_P - x_O). The line bundle attached by pointAddEquivPicZero to an affine point P is that of the divisor x_P - x_O, where x_P and x_O are the codimension-one points of projModel W corresponding to the place of K(W) at P and to the place at infinity.