The group law of the projective Weierstrass model

Let W be an elliptic Weierstrass curve over a commutative ring R, let E = projModel W be its projective model over S = Spec R, and regard E as the object Over.mk W.projModelOver of the cartesian monoidal category Over S, whose tensor product is the fibre product over S. This file makes E a commutative group object of Over S: a commutative group scheme over S. The unit is the zero section [0 : 1 : 0] (WeierstrassCurve.projModelZero), the multiplication is the Bosma–Lenstra addition morphism E ×_S E ⟶ E (WeierstrassCurve.additionMorphism), and the inverse is the negation morphism [X : Y : Z] ↦ [X : -Y - a₁X - a₃Z : Z] (WeierstrassCurve.projModelNeg).

The underlying commutative monoid object is WeierstrassCurve.monObjProjModelOver, whose axioms are the unit laws, associativity and commutativity of the addition morphism. The inverse laws are the right inverse law WeierstrassCurve.additionMorphism_right_inv and the left inverse law, which follows from it by commutativity WeierstrassCurve.additionMorphism_comm.

Over a field K, the points of this group scheme with values in Spec K form the group W.toAffine.Point of Mathlib: the dictionary WeierstrassCurve.projModelPointsEquiv between the sections of projModel W ⟶ Spec K and W.toAffine.Point carries the addition morphism to the addition of points (WeierstrassCurve.projModelPointsEquiv_lift_additionMorphism).

Main definitions

• WeierstrassCurve.grpObjProjModel: the group-object structure on Over.mk W.projModelOver.
• WeierstrassCurve.projModelPointsMulEquiv: over a field K, the isomorphism between the group of points of projModel W with values in Spec K and the group W.toAffine.Point.

Main results

• WeierstrassCurve.inv_projModelOver_left: the inverse is the negation morphism. The unit and multiplication are described by WeierstrassCurve.one_projModelOver_left and WeierstrassCurve.mul_projModelOver_left, and their commutativity is WeierstrassCurve.isCommMonObj_projModelOver.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §2.1.
• W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.
• AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), file projects/ModularCurves/ModularCurves/EllipticCurve/GroupLawConstruction.lean at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, which states the group laws of the same projective model as equations of morphisms of Over (Spec R) for its multiplication mulOver.

@[instance_reducible]

noncomputable instance WeierstrassCurve.grpObjProjModel {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.GrpObj (CategoryTheory.Over.mk W.projModelOver)

The group law of the projective Weierstrass model. For an elliptic Weierstrass curve W over a commutative ring R, the projective model projModel W ⟶ Spec R, as an object of the cartesian monoidal category Over (Spec R), is a group object: its unit is the zero section projModelZero, its multiplication is the Bosma–Lenstra addition morphism additionMorphism, and its inverse is the negation morphism projModelNeg.

@[simp]

theorem WeierstrassCurve.inv_projModelOver_left {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.Over.Hom.left CategoryTheory.GrpObj.inv = W.projModelNeg

The inverse of the group law of the projective Weierstrass model is the negation morphism.

The group of points over a field

noncomputable def WeierstrassCurve.projModelPointsMulEquiv {K : Type u} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk W.projModelOver) ≃* Multiplicative W.toAffine.Point

The group of points of the projective model over a field. For an elliptic Weierstrass curve W over a field K, the points of the group scheme projModel W with values in the base Spec K, with the group law of grpObjProjModel, form a group isomorphic to the group W.toAffine.Point of Mathlib. The isomorphism is the dictionary projModelPointsEquiv between sections of projModel W ⟶ Spec K and W.toAffine.Point, which is additive by projModelPointsEquiv_lift_additionMorphism.

@[simp]

theorem WeierstrassCurve.toAdd_projModelPointsMulEquiv {K : Type u} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk W.projModelOver) : Multiplicative.toAdd (W.projModelPointsMulEquiv x) = W.projModelPointsEquiv ⟨CategoryTheory.Over.Hom.left x, ⋯⟩

The point of W corresponding to a point x of the projective model over Spec K is the point corresponding to the section x.left of projModel W ⟶ Spec K under projModelPointsEquiv.

@[simp]

theorem WeierstrassCurve.projModelPointsMulEquiv_symm_apply_left {K : Type u} [Field K] [DecidableEq K] (W : WeierstrassCurve K) [W.IsElliptic] (P : Multiplicative W.toAffine.Point) : CategoryTheory.Over.Hom.left (W.projModelPointsMulEquiv.symm P) = ↑(W.projModelPointsEquiv.symm (Multiplicative.toAdd P))

The point of the projective model over Spec K corresponding to a point P of W is the section of projModel W ⟶ Spec K corresponding to P under projModelPointsEquiv.