The group law of an elliptic curve over a scheme

Let E be an elliptic curve over a scheme S, with structure morphism π : E ⟶ S, and regard E as the object Over.mk π 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, the multiplication is the addition morphism E ×_S E ⟶ E (EllipticCurveGeom.addition) and the inverse is the negation morphism E ⟶ E (EllipticCurveGeom.neg), both glued from the Bosma–Lenstra formulae of the local Weierstrass equations of E.

The group axioms are local on S, and over the base U of a pointed Weierstrass chart they are the group axioms of the projective model of the equation of the chart (WeierstrassCurve.grpObjProjModel). The argument is carried out on points. For T over S, the morphisms T ⟶ E over S form a commutative group, with the sum of x and y the composite of (x, y) : T ⟶ E ×_S E with the addition morphism. Restricting T to the base of a chart and reading points of E there as points of the projective model of the equation of the chart is injective jointly over all charts and carries the sum, the zero and the negation of points to those of the projective model, so the group axioms for points of E follow from those for points of the projective model. These groups are natural in T, so E represents a presheaf of commutative groups on Over S, and is therefore a commutative group object (CategoryTheory.CommGrpObj.ofRepresentableBy).

Main definitions

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.grpObj: the group-object structure on Over.mk E.structureMap.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isCommMonObj: the group law is commutative.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.one_left, TauCeti.AlgebraicGeometry.EllipticCurveGeom.mul_left and TauCeti.AlgebraicGeometry.EllipticCurveGeom.inv_left: the unit, multiplication and inverse are the zero section, the addition morphism and the negation morphism.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_one_left, TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_mul_left and TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_inv_left: in the group of points of E with values in an object of Over S, the zero, the product and the inverse are the zero section, the sum under the addition morphism and the negation.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.1–2.2.
• P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, II.1.

The zero section, addition and negation in Over S

Points of E read on a chart

The group law

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.grpObj {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.GrpObj (CategoryTheory.Over.mk E.structureMap)

The group law of an elliptic curve over a scheme. An elliptic curve E over a scheme S, as the object Over.mk E.structureMap of the cartesian monoidal category Over S, is a group object: its unit is the zero section, its multiplication is the addition morphism E ×_S E ⟶ E and its inverse is the negation morphism.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isCommMonObj {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.IsCommMonObj (CategoryTheory.Over.mk E.structureMap)

The group law of an elliptic curve over a scheme is commutative.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.one_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one = E.zero

The unit of the group law of an elliptic curve is the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mul_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul = E.addition

The multiplication of the group law of an elliptic curve is the addition morphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.inv_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.Over.Hom.left CategoryTheory.GrpObj.inv = E.neg

The inverse of the group law of an elliptic curve is the negation morphism.

The group of points

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_one_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : CategoryTheory.Over S} : CategoryTheory.Over.Hom.left 1 = CategoryTheory.CategoryStruct.comp Z.hom E.zero

The zero point of E with values in Z is the zero section over Z.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_mul_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : CategoryTheory.Over S} (x y : Z ⟶ CategoryTheory.Over.mk E.structureMap) : CategoryTheory.Over.Hom.left (x * y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.Over.Hom.left x) (CategoryTheory.Over.Hom.left y) ⋯) E.addition

The product of two points of E with values in Z is their sum under the addition morphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.hom_inv_left {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : CategoryTheory.Over S} (x : Z ⟶ CategoryTheory.Over.mk E.structureMap) : CategoryTheory.Over.Hom.left x⁻¹ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left x) E.neg

The inverse of a point of E with values in Z is its negation.