The addition morphism of an elliptic curve over a scheme

Let E be an elliptic curve over a scheme S, with structure morphism π : E ⟶ S and zero section 0. Zariski-locally on S, E is the projective model of an elliptic Weierstrass curve, through a pointed Weierstrass chart; the projective model carries the Bosma–Lenstra addition morphism WeierstrassCurve.additionMorphism. This file glues these local addition morphisms to the addition morphism E ×_S E ⟶ E over S.

A pointed Weierstrass chart c, over an open U = base ⟶ S, presents the restriction E_U of E as the projective model of its equation. Transporting the addition morphism of the equation along this presentation gives the addition of the chart E_U ×_U E_U ⟶ E_U (PointedWeierstrassChart.addition). The additions of two charts agree where both are defined. Over an affine open V of the base of a chart c, the restriction c.restrict V is again a chart, and the comparison of the two charts over V is a morphism of projective models which carries the zero section to the zero section and is a base change square. The Bosma–Lenstra addition morphism commutes with such morphisms (WeierstrassCurve.additionMorphism_comp_of_isPullback), because a pointed isomorphism of projective models over an affine base is induced by a change of variables. So the addition of every chart restricts to the addition of each of its restrictions to affine opens, and two charts c and d agree near every point of U_c ∩ U_d, through a restriction of c to an affine open mapping into U_d.

The parts E_U ×_U E_U of E ×_S E over the bases of all pointed Weierstrass charts form an open cover, and the additions of the charts glue along it (EllipticCurveGeom.glueMorphisms) to EllipticCurveGeom.addition. Its restriction to every chart is the addition of the chart (EllipticCurveGeom.pullbackMap_addition), and this characterises it among all morphisms E ×_S E ⟶ E, already on the charts of any one atlas (EllipticCurveGeom.eq_addition_of_atlas). In particular the addition morphism does not depend on the choice of local Weierstrass equations.

Main definitions

• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition c: the addition of a pointed Weierstrass chart, the Bosma–Lenstra addition morphism of its equation transported to the restriction of the curve to the base of the chart.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.addition E: the addition morphism E ×_S E ⟶ E of an elliptic curve over a scheme.

Main results

• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition_pullbackCarrierMap: the addition of a chart restricts, over a chart whose base maps into its base, to the addition of that chart.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.pullbackMap_addition: on the restriction of E ×_S E to the base of any pointed Weierstrass chart, the addition morphism is the addition of the chart.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.addition_structureMap: the addition morphism lies over S.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_addition_of_atlas: a morphism E ×_S E ⟶ E that restricts to the addition of every chart of a pointed Weierstrass atlas is the addition morphism.

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.
• W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.

The addition of a chart

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.Limits.pullback c.toBase c.toBase ⟶ c.pullbackCarrier

The addition of a pointed Weierstrass chart c of π : X ⟶ S: the morphism X_U ×_U X_U ⟶ X_U, for X_U the restriction of X to the base U of the chart, obtained by transporting the Bosma–Lenstra addition morphism of the equation of c along the isomorphism of X_U with its projective model (addition_modelIso_hom).

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition_modelIso_hom {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.CategoryStruct.comp c.addition c.modelIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map c.toBase c.toBase c.equation.projModelOver c.equation.projModelOver c.modelIso.hom c.modelIso.hom c.baseIso.hom ⋯ ⋯) c.equation.additionMorphism

Through the isomorphism of the restriction of the curve to the base of a chart with the projective model of its equation, the addition of the chart is the Bosma–Lenstra addition morphism of the equation.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition_modelIso_hom_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : c.equation.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp c.addition (CategoryTheory.CategoryStruct.comp c.modelIso.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map c.toBase c.toBase c.equation.projModelOver c.equation.projModelOver c.modelIso.hom c.modelIso.hom c.baseIso.hom ⋯ ⋯) (CategoryTheory.CategoryStruct.comp c.equation.additionMorphism h)

Through the isomorphism of the restriction of the curve to the base of a chart with the projective model of its equation, the addition of the chart is the Bosma–Lenstra addition morphism of the equation.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition_toBase {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.CategoryStruct.comp c.addition c.toBase = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst c.toBase c.toBase) c.toBase

The addition of a chart lies over the base of the chart.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition_toBase_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : c.base ⟶ Z) : CategoryTheory.CategoryStruct.comp c.addition (CategoryTheory.CategoryStruct.comp c.toBase h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst c.toBase c.toBase) (CategoryTheory.CategoryStruct.comp c.toBase h)

The addition of a chart lies over the base of the chart.

Restriction of the addition of a chart

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition_pullbackCarrierMap {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) : CategoryTheory.CategoryStruct.comp k.addition (pullbackCarrierMap hh) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map k.toBase k.toBase c.toBase c.toBase (pullbackCarrierMap hh) (pullbackCarrierMap hh) h ⋯ ⋯) c.addition

Restriction of the addition of a chart. If the base of a chart k maps to the base of a chart c over S, the addition of c restricts to the addition of k. Both are the Bosma–Lenstra addition morphisms of their equations; the comparison of the projective models of the two equations is a base change square carrying the zero section to the zero section, and the addition morphism commutes with it (WeierstrassCurve.additionMorphism_comp_of_isPullback).

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.addition_pullbackCarrierMap_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} {k c : PointedWeierstrassChart π zero} {h : k.base ⟶ c.base} (hh : CategoryTheory.CategoryStruct.comp h c.baseMap = k.baseMap) {Z : AlgebraicGeometry.Scheme} (h✝ : c.pullbackCarrier ⟶ Z) : CategoryTheory.CategoryStruct.comp k.addition (CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map k.toBase k.toBase c.toBase c.toBase (pullbackCarrierMap hh) (pullbackCarrierMap hh) h ⋯ ⋯) (CategoryTheory.CategoryStruct.comp c.addition h✝)

Restriction of the addition of a chart. If the base of a chart k maps to the base of a chart c over S, the addition of c restricts to the addition of k. Both are the Bosma–Lenstra addition morphisms of their equations; the comparison of the projective models of the two equations is a base change square carrying the zero section to the zero section, and the addition morphism commutes with it (WeierstrassCurve.additionMorphism_comp_of_isPullback).

Gluing the additions of the charts

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.addition {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.Limits.pullback E.structureMap E.structureMap ⟶ E.carrier

The addition morphism E ×_S E ⟶ E of an elliptic curve E over a scheme S: the morphism whose restriction to the base U of every pointed Weierstrass chart is the Bosma–Lenstra addition morphism of the equation of the chart (pullbackMap_addition). It is glued from these local addition morphisms, which agree where they overlap, and it lies over S (addition_structureMap).

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.pullbackMap_addition {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (c : PointedWeierstrassChart E.structureMap E.zero) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map c.toBase c.toBase E.structureMap E.structureMap c.toTotal c.toTotal c.baseMap ⋯ ⋯) E.addition = CategoryTheory.CategoryStruct.comp c.addition c.toTotal

The addition morphism on a chart. On the restriction of E ×_S E to the base of a pointed Weierstrass chart c, the addition morphism of E is the addition of the chart, the Bosma–Lenstra addition morphism of the equation of c.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.pullbackMap_addition_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (c : PointedWeierstrassChart E.structureMap E.zero) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map c.toBase c.toBase E.structureMap E.structureMap c.toTotal c.toTotal c.baseMap ⋯ ⋯) (CategoryTheory.CategoryStruct.comp E.addition h) = CategoryTheory.CategoryStruct.comp c.addition (CategoryTheory.CategoryStruct.comp c.toTotal h)

The addition morphism on a chart. On the restriction of E ×_S E to the base of a pointed Weierstrass chart c, the addition morphism of E is the addition of the chart, the Bosma–Lenstra addition morphism of the equation of c.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.addition_structureMap {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.CategoryStruct.comp E.addition E.structureMap = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst E.structureMap E.structureMap) E.structureMap

The addition morphism of an elliptic curve over S lies over S.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.addition_structureMap_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp E.addition (CategoryTheory.CategoryStruct.comp E.structureMap h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst E.structureMap E.structureMap) (CategoryTheory.CategoryStruct.comp E.structureMap h)

The addition morphism of an elliptic curve over S lies over S.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_addition_of_atlas {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (A : PointedWeierstrassAtlas E.structureMap E.zero) {μ : CategoryTheory.Limits.pullback E.structureMap E.structureMap ⟶ E.carrier} (hμ : ∀ (i : A.index), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (A.chart i).toBase (A.chart i).toBase E.structureMap E.structureMap (A.chart i).toTotal (A.chart i).toTotal (A.chart i).baseMap ⋯ ⋯) μ = CategoryTheory.CategoryStruct.comp (A.chart i).addition (A.chart i).toTotal) : μ = E.addition

Uniqueness of the addition morphism. A morphism μ : E ×_S E ⟶ E whose restriction to the base of every chart of a pointed Weierstrass atlas is the addition of the chart is the addition morphism of E.