The projective Weierstrass model as a commutative monoid object

Let W be an elliptic Weierstrass curve over a commutative ring R, let E = projModel W be its projective model and let S = Spec R. Group schemes over S are group objects in the cartesian monoidal category Over S, whose tensor product is the fibre product over S. This file makes E, as the object Over.mk W.projModelOver of Over S, a commutative monoid object: the unit is the zero section [0 : 1 : 0] and the multiplication is the Bosma–Lenstra addition morphism E ×_S E ⟶ E. The monoid axioms are the unit laws, associativity and commutativity of the addition morphism, read through the description of the cartesian monoidal structure of Over S by fibre products (CategoryTheory.Over.lift_left and its companions).

The monoid object is compatible with base change. For a ring homomorphism f : R →+* R', the projective model of W.map f over Spec R' is isomorphic, as an object of Over (Spec R'), to the image of Over.mk W.projModelOver under the pullback functor along Spec f (WeierstrassCurve.projModelOverBaseChangeIso, from the base change square WeierstrassCurve.isPullback_projModelBaseChange). The pullback functor carries the monoid object of W to a monoid object over Spec R' (CategoryTheory.Functor.monObjObj), and the isomorphism is a homomorphism of monoid objects.

Main definitions

• WeierstrassCurve.monObjProjModelOver: the monoid object structure on Over.mk W.projModelOver, with unit the zero section and multiplication the addition morphism.

Main results

• WeierstrassCurve.isCommMonObj_projModelOver: the monoid object is commutative.
• WeierstrassCurve.one_projModelOver_left and WeierstrassCurve.mul_projModelOver_left: the underlying morphisms of schemes of the unit and the multiplication are the zero section and the addition morphism.
• WeierstrassCurve.isMonHom_projModelOverBaseChangeIso_hom: the base change isomorphism is a homomorphism of monoid objects.

References

• N. 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.

Provenance

The monoid part of AINTLIB's modelGrpObj (github.com/CBirkbeck/AINTLIB, Apache-2.0, commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/ModelRecord.lean) is the same structure, with its axioms proved in Over (Spec R) directly. Here the axioms are deduced from the laws of the addition morphism as morphisms of schemes. The compatibility with base change corresponds to isMonHom_modelBaseChangeIso (file AffineSectionSpecPoints.lean in the same directory), which compares the source's model with its base change of elliptic curves; here the comparison is with the pullback functor Over.pullback, and the two axioms are checked on the two projections of the fibre product, using WeierstrassCurve.additionMorphism_projModelBaseChange.

@[instance_reducible]

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

The projective model of an elliptic Weierstrass curve W over R, as an object of Over (Spec R), is a monoid object of the cartesian monoidal category Over (Spec R): its unit is the zero section projModelZero W and its multiplication is the Bosma–Lenstra addition morphism additionMorphism W (one_projModelOver_left, mul_projModelOver_left).

@[simp]

theorem WeierstrassCurve.one_projModelOver_left {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one = W.projModelZero

The unit of the monoid object Over.mk W.projModelOver is the zero section.

@[simp]

theorem WeierstrassCurve.mul_projModelOver_left {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul = W.additionMorphism

The multiplication of the monoid object Over.mk W.projModelOver is the Bosma–Lenstra addition morphism.

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

The monoid object Over.mk W.projModelOver is commutative, because the addition morphism is invariant under swapping its two factors (additionMorphism_comm).

instance WeierstrassCurve.isMonHom_projModelOverBaseChangeIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) {R' : Type u} [CommRing R'] (f : R →+* R') [W.IsElliptic] : CategoryTheory.IsMonHom (W.projModelOverBaseChangeIso f).hom

The monoid object commutes with base change. The base change isomorphism projModelOverBaseChangeIso W f is a homomorphism from the monoid object of W.map f to the image of the monoid object of W under the pullback functor along Spec f, whose monoid structure is CategoryTheory.Functor.monObjObj (a scoped instance, in CategoryTheory.Obj).