The negation 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 negation morphism WeierstrassCurve.projModelNeg, [X : Y : Z] ↦ [X : -Y - a₁X - a₃Z : Z]. This file glues these local negation morphisms to the negation morphism 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 negation morphism of the equation along this presentation gives the negation of the chart E_U ⟶ E_U (PointedWeierstrassChart.neg). If the base of a chart k maps to the base of a chart c over S, the comparison of the two projective models carries the zero section to the zero section and is a base change square, so it commutes with negation (WeierstrassCurve.projModelNeg_comp_of_isPullback). The negations of the charts therefore glue along the cover of E by the restrictions E_U (EllipticCurveGeom.glueMorphisms) to EllipticCurveGeom.neg. Its restriction to every chart is the negation of the chart (EllipticCurveGeom.toTotal_neg), and this characterises it among all morphisms E ⟶ E, already on the charts of any one atlas (EllipticCurveGeom.eq_neg_of_atlas). In particular the negation morphism does not depend on the choice of local Weierstrass equations. Like its local models, it is an involution over S that fixes the zero section.

Main definitions

• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg c: the negation of a pointed Weierstrass chart, the negation morphism of its equation transported to the restriction of the curve to the base of the chart.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg E: the negation morphism E ⟶ E of an elliptic curve over a scheme.

Main results

• TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_pullbackCarrierMap: the negation of a chart restricts, over a chart whose base maps into its base, to the negation of that chart.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.toTotal_neg: on the restriction of E to the base of any pointed Weierstrass chart, the negation morphism is the negation of the chart.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.modelPoint_neg: on a chart, the model point of -P is the negative of the model point of P.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_neg_of_atlas: a morphism E ⟶ E that restricts to the negation of every chart of a pointed Weierstrass atlas is the negation morphism.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_structureMap, TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_neg and TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_neg: the negation morphism lies over S, fixes the zero section and is an involution; in particular it is an isomorphism, its own inverse.

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 negation of a chart

noncomputable def TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : c.pullbackCarrier ⟶ c.pullbackCarrier

The negation of a pointed Weierstrass chart c of π : X ⟶ S: the morphism X_U ⟶ X_U, for X_U the restriction of X to the base U of the chart, obtained by transporting the negation morphism of the projective model of the equation of c along the isomorphism of X_U with that model (neg_modelIso_hom).

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_modelIso_hom {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.CategoryStruct.comp c.neg c.modelIso.hom = CategoryTheory.CategoryStruct.comp c.modelIso.hom c.equation.projModelNeg

Through the isomorphism of the restriction of the curve to the base of a chart with the projective model of its equation, the negation of the chart is the negation morphism of the projective model.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_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.neg (CategoryTheory.CategoryStruct.comp c.modelIso.hom h) = CategoryTheory.CategoryStruct.comp c.modelIso.hom (CategoryTheory.CategoryStruct.comp c.equation.projModelNeg h)

Through the isomorphism of the restriction of the curve to the base of a chart with the projective model of its equation, the negation of the chart is the negation morphism of the projective model.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_toBase {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.CategoryStruct.comp c.neg c.toBase = c.toBase

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

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_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.neg (CategoryTheory.CategoryStruct.comp c.toBase h) = CategoryTheory.CategoryStruct.comp c.toBase h

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

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pulledZero_neg {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.CategoryStruct.comp c.pulledZero c.neg = c.pulledZero

The negation of a chart fixes the section induced by the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.pulledZero_neg_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : c.pullbackCarrier ⟶ Z) : CategoryTheory.CategoryStruct.comp c.pulledZero (CategoryTheory.CategoryStruct.comp c.neg h) = CategoryTheory.CategoryStruct.comp c.pulledZero h

The negation of a chart fixes the section induced by the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_neg {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) : CategoryTheory.CategoryStruct.comp c.neg c.neg = CategoryTheory.CategoryStruct.id c.pullbackCarrier

The negation of a chart is an involution.

@[simp]

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_neg_assoc {S X : AlgebraicGeometry.Scheme} {π : X ⟶ S} {zero : S ⟶ X} (c : PointedWeierstrassChart π zero) {Z : AlgebraicGeometry.Scheme} (h : c.pullbackCarrier ⟶ Z) : CategoryTheory.CategoryStruct.comp c.neg (CategoryTheory.CategoryStruct.comp c.neg h) = h

The negation of a chart is an involution.

Restriction of the negation of a chart

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_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.neg (pullbackCarrierMap hh) = CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) c.neg

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

theorem TauCeti.AlgebraicGeometry.PointedWeierstrassChart.neg_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.neg (CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) h✝) = CategoryTheory.CategoryStruct.comp (pullbackCarrierMap hh) (CategoryTheory.CategoryStruct.comp c.neg h✝)

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

Gluing the negations of the charts

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : E.carrier ⟶ E.carrier

The negation morphism 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 negation morphism [X : Y : Z] ↦ [X : -Y - a₁X - a₃Z : Z] of the projective model of the equation of the chart (toTotal_neg). It is glued from these local negation morphisms, which agree where they overlap.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.toTotal_neg {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (c : PointedWeierstrassChart E.structureMap E.zero) : CategoryTheory.CategoryStruct.comp c.toTotal E.neg = CategoryTheory.CategoryStruct.comp c.neg c.toTotal

The negation morphism on a chart. On the restriction of E to the base of a pointed Weierstrass chart c, the negation morphism of E is the negation of the chart, the negation morphism of the projective model of the equation of c.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.toTotal_neg_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (c : PointedWeierstrassChart E.structureMap E.zero) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp c.toTotal (CategoryTheory.CategoryStruct.comp E.neg h) = CategoryTheory.CategoryStruct.comp c.neg (CategoryTheory.CategoryStruct.comp c.toTotal h)

The negation morphism on a chart. On the restriction of E to the base of a pointed Weierstrass chart c, the negation morphism of E is the negation of the chart, the negation morphism of the projective model of the equation of c.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_neg_of_atlas {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (A : PointedWeierstrassAtlas E.structureMap E.zero) {ν : E.carrier ⟶ E.carrier} (hν : ∀ (i : A.index), CategoryTheory.CategoryStruct.comp (A.chart i).toTotal ν = CategoryTheory.CategoryStruct.comp (A.chart i).neg (A.chart i).toTotal) : ν = E.neg

Uniqueness of the negation morphism. A morphism ν : E ⟶ E whose restriction to the base of every chart of a pointed Weierstrass atlas is the negation of the chart is the negation morphism of E.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_structureMap {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.CategoryStruct.comp E.neg E.structureMap = E.structureMap

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

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_structureMap_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp E.neg (CategoryTheory.CategoryStruct.comp E.structureMap h) = CategoryTheory.CategoryStruct.comp E.structureMap h

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

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.modelPoint_neg {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (c : PointedWeierstrassChart E.structureMap E.zero) {P : S ⟶ E.carrier} (hP : CategoryTheory.CategoryStruct.comp P E.structureMap = CategoryTheory.CategoryStruct.id S) : c.modelPoint ⋯ = CategoryTheory.CategoryStruct.comp (c.modelPoint hP) c.equation.projModelNeg

The model point of the negative P ≫ E.neg of a section P is the negative of its model point.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_neg {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.CategoryStruct.comp E.zero E.neg = E.zero

The negation morphism of an elliptic curve fixes the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.zero_neg_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp E.zero (CategoryTheory.CategoryStruct.comp E.neg h) = CategoryTheory.CategoryStruct.comp E.zero h

The negation morphism of an elliptic curve fixes the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_neg {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.CategoryStruct.comp E.neg E.neg = CategoryTheory.CategoryStruct.id E.carrier

The negation morphism of an elliptic curve is an involution.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.neg_neg_assoc {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp E.neg (CategoryTheory.CategoryStruct.comp E.neg h) = h

The negation morphism of an elliptic curve is an involution.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.isIso_neg {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.IsIso E.neg

The negation morphism of an elliptic curve is an isomorphism, being an involution.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.inv_neg {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) : CategoryTheory.inv E.neg = E.neg

The negation morphism of an elliptic curve is its own inverse.