The negation morphism of the projective Weierstrass model

Let W be a Weierstrass curve over a commutative ring R. The change of variables negVariableChange W = ⟨-1, 0, -a₁, -a₃⟩ fixes W, so the isomorphism projModelVariableChangeIso W (negVariableChange W) it induces is, through negVariableChange W • W = W, an automorphism of the projective Weierstrass model projModel W: the negation morphism projModelNeg W, [X : Y : Z] ↦ [X : -Y - a₁X - a₃Z : Z]. It is an involution over Spec R fixing the zero section, which on points with homogeneous coordinates P is Mathlib's negation WeierstrassCurve.Projective.neg, [P₀ : P₁ : P₂] ↦ [P₀ : -P₁ - a₁P₀ - a₃P₂ : P₂], and it commutes with base change and with the isomorphisms induced by changes of variables. No ellipticity is needed.

Since every pointed isomorphism of projective models over the same base is induced by a change of variables (WeierstrassCurve.existsUnique_eq_eqToHom_comp_projModelVariableChangeIso_hom), negation commutes with every morphism of projective models that carries the zero section to the zero section and is a base change square. This makes the negation of an elliptic curve over a scheme independent of the local Weierstrass equations used to define it.

Main definitions

• WeierstrassCurve.projModelNeg W: the negation morphism projModel W ⟶ projModel W.

Main results

• WeierstrassCurve.projModelNeg_projModelOver: negation lies over Spec R.
• WeierstrassCurve.projModelZero_projModelNeg: negation fixes the zero section.
• WeierstrassCurve.projModelNeg_projModelNeg: negation is an involution.
• WeierstrassCurve.isIso_projModelNeg: negation is an isomorphism, its own inverse (WeierstrassCurve.inv_projModelNeg).
• WeierstrassCurve.projModelPoint_projModelNeg: negation sends the point with homogeneous coordinates P to the point with homogeneous coordinates Projective.neg P.
• WeierstrassCurve.projModelAffinePoint_projModelNeg: negation sends the point [x : y : 1] to [x : -y - a₁x - a₃ : 1].
• WeierstrassCurve.projModelAffinePoint_apply_eq_or_eq_projModelNeg_iff: over a point s of Spec R, the point [x₂ : y₂ : 1] is ±[x₁ : y₁ : 1] exactly when x₂ ≡ x₁ modulo s.
• WeierstrassCurve.projModelNeg_projModelBaseChange: negation commutes with the base change morphism projModel (W.map f) ⟶ projModel W.
• WeierstrassCurve.projModelNeg_projModelVariableChangeIso_hom: negation commutes with the isomorphism projModel (C • W) ≅ projModel W induced by a change of variables C.
• WeierstrassCurve.projModelNeg_comp_hom_of_iso: negation commutes with every pointed isomorphism of projective models over Spec R.
• WeierstrassCurve.projModelNeg_comp_of_isPullback: negation commutes with every pointed cartesian morphism of projective models.
• WeierstrassCurve.eq_id_of_projModelAffinePoint_comp_eq: an automorphism of the projective model over Spec R fixing the zero section and two affine points (x₁, y₁), (x₂, y₂), with x₁ - x₂ and 2y₁ + a₁x₁ + a₃ units, is the identity.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.2

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/GroupLawConstruction.lean, declarations negVec, negGradedQuot, negModelHom, negModelHom_π, negModelHom_negModelHom, negModelHom_zero and negModelHom_specPoints. Here the morphism is the isomorphism WeierstrassCurve.projModelVariableChangeIso induced by the change of variables negVariableChange, in place of Proj of the source's substitution negVec; the zero section is fixed because every such isomorphism preserves it, in place of the source's rescaling automorphism allNegGradedQuot; and the points are those of projModelPoint, for an arbitrary ring homomorphism g : R →+* S and a solution with a unit coordinate, in place of the source's field points matched with W.toAffine.Point.

noncomputable def WeierstrassCurve.projModelNeg {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.projModel ⟶ W.projModel

The negation morphism [X : Y : Z] ↦ [X : -Y - a₁X - a₃Z : Z] of the projective Weierstrass model, (x, y) ↦ (x, -y - a₁x - a₃) on the affine part: the isomorphism projModel (negVariableChange W • W) ≅ projModel W induced by the change of variables negVariableChange W, read on projModel W through negVariableChange W • W = W. It acts on homogeneous coordinates by Projective.neg (projModelPoint_projModelNeg).

@[simp]

theorem WeierstrassCurve.projModelNeg_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CategoryTheory.CategoryStruct.comp W.projModelNeg W.projModelOver = W.projModelOver

The negation morphism lies over the base Spec R.

@[simp]

theorem WeierstrassCurve.projModelNeg_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp W.projModelNeg (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp W.projModelOver h

The negation morphism lies over the base Spec R.

@[simp]

theorem WeierstrassCurve.projModelZero_projModelNeg {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CategoryTheory.CategoryStruct.comp W.projModelZero W.projModelNeg = W.projModelZero

The negation morphism fixes the zero section: [0 : 1 : 0] ↦ [0 : -1 : 0] = [0 : 1 : 0].

@[simp]

theorem WeierstrassCurve.projModelZero_projModelNeg_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp W.projModelZero (CategoryTheory.CategoryStruct.comp W.projModelNeg h) = CategoryTheory.CategoryStruct.comp W.projModelZero h

The negation morphism fixes the zero section: [0 : 1 : 0] ↦ [0 : -1 : 0] = [0 : 1 : 0].

@[simp]

theorem WeierstrassCurve.projModelNeg_projModelNeg {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CategoryTheory.CategoryStruct.comp W.projModelNeg W.projModelNeg = CategoryTheory.CategoryStruct.id W.projModel

The negation morphism is an involution.

@[simp]

theorem WeierstrassCurve.projModelNeg_projModelNeg_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp W.projModelNeg (CategoryTheory.CategoryStruct.comp W.projModelNeg h) = h

The negation morphism is an involution.

instance WeierstrassCurve.isIso_projModelNeg {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CategoryTheory.IsIso W.projModelNeg

The negation morphism is an isomorphism, being an involution.

@[simp]

theorem WeierstrassCurve.inv_projModelNeg {R : Type u} [CommRing R] (W : WeierstrassCurve R) : CategoryTheory.inv W.projModelNeg = W.projModelNeg

The negation morphism is its own inverse.

theorem WeierstrassCurve.projModelPoint_projModelNeg {R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} {hP : (W.toProjective.map g).Equation P} {i : Fin 3} (hi : IsUnit (P i)) {j : Fin 3} (hj : IsUnit ((W.toProjective.map g).neg P j)) : CategoryTheory.CategoryStruct.comp (W.projModelPoint g hP hi) W.projModelNeg = W.projModelPoint g ⋯ hj

The negation morphism sends the point projModelPoint W g hP hi with homogeneous coordinates P to the point with homogeneous coordinates Projective.neg P = [P₀ : -P₁ - a₁P₀ - a₃P₂ : P₂], the negation for the curve W.map g, defined through any chart D₊(Xⱼ) on which (Projective.neg P)ⱼ is a unit. Negation fixes P₀ and P₂ (Projective.neg_X, Projective.neg_Z), so for j ≠ 1 the hypothesis hj says that Pⱼ is a unit.

theorem WeierstrassCurve.projModelPoint_projModelNeg_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {S : Type u} [CommRing S] {g : R →+* S} {P : Fin 3 → S} {hP : (W.toProjective.map g).Equation P} {i : Fin 3} (hi : IsUnit (P i)) {j : Fin 3} (hj : IsUnit ((W.toProjective.map g).neg P j)) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.projModelPoint g hP hi) (CategoryTheory.CategoryStruct.comp W.projModelNeg h) = CategoryTheory.CategoryStruct.comp (W.projModelPoint g ⋯ hj) h

The negation morphism sends the point projModelPoint W g hP hi with homogeneous coordinates P to the point with homogeneous coordinates Projective.neg P = [P₀ : -P₁ - a₁P₀ - a₃P₂ : P₂], the negation for the curve W.map g, defined through any chart D₊(Xⱼ) on which (Projective.neg P)ⱼ is a unit. Negation fixes P₀ and P₂ (Projective.neg_X, Projective.neg_Z), so for j ≠ 1 the hypothesis hj says that Pⱼ is a unit.

@[simp]

theorem WeierstrassCurve.projModelAffinePoint_projModelNeg {R : Type u} [CommRing R] (W : WeierstrassCurve R) {x y : R} (h : W.toAffine.Equation x y) : CategoryTheory.CategoryStruct.comp (W.projModelAffinePoint h) W.projModelNeg = W.projModelAffinePoint ⋯

The negation morphism sends the point [x : y : 1] with values in R to the point [x : -y - a₁x - a₃ : 1], the negative of (x, y) on the affine curve.

@[simp]

theorem WeierstrassCurve.projModelAffinePoint_projModelNeg_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {x y : R} (h : W.toAffine.Equation x y) {Z : AlgebraicGeometry.Scheme} (h✝ : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.projModelAffinePoint h) (CategoryTheory.CategoryStruct.comp W.projModelNeg h✝) = CategoryTheory.CategoryStruct.comp (W.projModelAffinePoint ⋯) h✝

The negation morphism sends the point [x : y : 1] with values in R to the point [x : -y - a₁x - a₃ : 1], the negative of (x, y) on the affine curve.

theorem WeierstrassCurve.projModelAffinePoint_apply_eq_or_eq_projModelNeg_iff {R : Type u} [CommRing R] (W : WeierstrassCurve R) {x₁ y₁ x₂ y₂ : R} (h₁ : W.toAffine.Equation x₁ y₁) (h₂ : W.toAffine.Equation x₂ y₂) (s : ↥(AlgebraicGeometry.Spec ↧R)) : (W.projModelAffinePoint h₂) s = (W.projModelAffinePoint h₁) s ∨ (W.projModelAffinePoint h₂) s = (CategoryTheory.CategoryStruct.comp (W.projModelAffinePoint h₁) W.projModelNeg) s ↔ x₂ - x₁ ∈ s.asIdeal

Over a point s of Spec R, the point [x₂ : y₂ : 1] is [x₁ : y₁ : 1] or its negative exactly when x₂ ≡ x₁ modulo s.

@[simp]

theorem WeierstrassCurve.projModelNeg_projModelBaseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) {R' : Type u} [CommRing R'] (f : R →+* R') : CategoryTheory.CategoryStruct.comp (W.map f).projModelNeg (W.projModelBaseChange f) = CategoryTheory.CategoryStruct.comp (W.projModelBaseChange f) W.projModelNeg

The negation morphism commutes with base change: negation on projModel (W.map f) followed by the base change morphism projModel (W.map f) ⟶ projModel W along f : R →+* R' is the base change morphism followed by negation on projModel W.

@[simp]

theorem WeierstrassCurve.projModelNeg_projModelBaseChange_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) {R' : Type u} [CommRing R'] (f : R →+* R') {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.map f).projModelNeg (CategoryTheory.CategoryStruct.comp (W.projModelBaseChange f) h) = CategoryTheory.CategoryStruct.comp (W.projModelBaseChange f) (CategoryTheory.CategoryStruct.comp W.projModelNeg h)

The negation morphism commutes with base change: negation on projModel (W.map f) followed by the base change morphism projModel (W.map f) ⟶ projModel W along f : R →+* R' is the base change morphism followed by negation on projModel W.

@[simp]

theorem WeierstrassCurve.projModelNeg_projModelVariableChangeIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) : CategoryTheory.CategoryStruct.comp (C • W).projModelNeg (W.projModelVariableChangeIso C).hom = CategoryTheory.CategoryStruct.comp (W.projModelVariableChangeIso C).hom W.projModelNeg

The negation morphism commutes with the isomorphism projModel (C • W) ≅ projModel W induced by a change of variables C: negation on projModel (C • W) followed by the isomorphism is the isomorphism followed by negation on projModel W.

@[simp]

theorem WeierstrassCurve.projModelNeg_projModelVariableChangeIso_hom_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (C • W).projModelNeg (CategoryTheory.CategoryStruct.comp (W.projModelVariableChangeIso C).hom h) = CategoryTheory.CategoryStruct.comp (W.projModelVariableChangeIso C).hom (CategoryTheory.CategoryStruct.comp W.projModelNeg h)

The negation morphism commutes with the isomorphism projModel (C • W) ≅ projModel W induced by a change of variables C: negation on projModel (C • W) followed by the isomorphism is the isomorphism followed by negation on projModel W.

theorem WeierstrassCurve.projModelNeg_comp_hom_of_iso {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} (e : W.projModel ≅ W'.projModel) (he : CategoryTheory.CategoryStruct.comp e.hom W'.projModelOver = W.projModelOver) (h0 : CategoryTheory.CategoryStruct.comp W.projModelZero e.hom = W'.projModelZero) : CategoryTheory.CategoryStruct.comp W.projModelNeg e.hom = CategoryTheory.CategoryStruct.comp e.hom W'.projModelNeg

Negation commutes with pointed isomorphisms. An isomorphism e : projModel W ≅ projModel W' of projective Weierstrass models over Spec R, carrying the zero section to the zero section, carries the negation morphism of W to that of W'.

theorem WeierstrassCurve.projModelNeg_comp_of_isPullback {R R' : Type u} [CommRing R] [CommRing R'] {W : WeierstrassCurve R} {W' : WeierstrassCurve R'} {F : W.projModel ⟶ W'.projModel} {ψ : AlgebraicGeometry.Spec ↧R ⟶ AlgebraicGeometry.Spec ↧R'} (hF : CategoryTheory.IsPullback F W.projModelOver W'.projModelOver ψ) (h0 : CategoryTheory.CategoryStruct.comp W.projModelZero F = CategoryTheory.CategoryStruct.comp ψ W'.projModelZero) : CategoryTheory.CategoryStruct.comp W.projModelNeg F = CategoryTheory.CategoryStruct.comp F W'.projModelNeg

Negation commutes with pointed cartesian morphisms. Let F : projModel W ⟶ projModel W' be a morphism of projective Weierstrass models over R and R', lying over ψ : Spec R ⟶ Spec R', such that the square formed by F, the structure morphisms and ψ is a pullback square, and carrying the zero section to the zero section. Then F carries the negation morphism of W to that of W'.

theorem WeierstrassCurve.eq_id_of_projModelAffinePoint_comp_eq {R : Type u} [CommRing R] {W : WeierstrassCurve R} {e : W.projModel ⟶ W.projModel} (he : CategoryTheory.IsPullback e W.projModelOver W.projModelOver (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R))) (h0 : CategoryTheory.CategoryStruct.comp W.projModelZero e = W.projModelZero) {x₁ y₁ x₂ y₂ : R} (h₁ : W.toAffine.Equation x₁ y₁) (h₂ : W.toAffine.Equation x₂ y₂) (hx : IsUnit (x₁ - x₂)) (hy : IsUnit (y₁ - W.toAffine.negY x₁ y₁)) (he₁ : CategoryTheory.CategoryStruct.comp (W.projModelAffinePoint h₁) e = W.projModelAffinePoint h₁) (he₂ : CategoryTheory.CategoryStruct.comp (W.projModelAffinePoint h₂) e = W.projModelAffinePoint h₂) : e = CategoryTheory.CategoryStruct.id W.projModel

An automorphism of the projective model fixing two suitable points is the identity. Let e : projModel W ⟶ projModel W be an automorphism over Spec R, given as a cartesian square over the identity, which fixes the zero section and the points [x₁ : y₁ : 1] and [x₂ : y₂ : 1]. If x₁ - x₂ and y₁ - (-y₁ - a₁x₁ - a₃) are units, then e is the identity. Over a field, the conditions say that the two points are distinct from each other and from the negative of the first point, and that the first point is not its own negative.