The unit law for the projective Weierstrass addition morphism

Let W be an elliptic Weierstrass curve over a commutative ring R, let E = projModel W, and let S = Spec R. This file proves that the zero section is a right and a left identity for the Bosma–Lenstra addition morphism E ×_S E ⟶ E.

The proof is scheme-theoretic over an arbitrary base. The standard charts D₊(Y) and D₊(Z) cover E: the complement of D₊(Z) is exactly the zero section, which lies in D₊(Y). On D₊(Z), the addition law attached to Z = 0 evaluates at (P, [0 : 1 : 0]) to -P₂ • P; on D₊(Y), the law attached to Y = 0 evaluates to P₁ • P. The chosen chart coordinate is one in each case, so both laws define the original projective point. The left unit law follows from the right one, because the addition morphism is commutative (WeierstrassCurve.additionMorphism_comm).

Main results

• WeierstrassCurve.additionMorphism_right_unit: adding the zero section on the right is the identity morphism of projModel W.
• WeierstrassCurve.additionMorphism_left_unit: adding the zero section on the left is the identity morphism of projModel W.

References

• W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.
• AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), mulOver_oneOver in projects/ModularCurves/ModularCurves/EllipticCurve/GroupLawAxioms.lean at commit c3415f32a313e19ace43e05479aeaa0d56ca287a: a formalization of the same right unit law, proved by descent from a universal atlas and field-valued points rather than on two affine charts. The left unit law is deduced from the right one and commutativity as in oneOver_mulOver, in the same file.

@[simp]

theorem WeierstrassCurve.additionMorphism_right_unit {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id W.projModel) (CategoryTheory.CategoryStruct.comp W.projModelOver W.projModelZero) ⋯) W.additionMorphism = CategoryTheory.CategoryStruct.id W.projModel

The zero section is a right identity for the Bosma–Lenstra addition morphism on the projective Weierstrass model. This is an equality of scheme morphisms over an arbitrary commutative base ring; in particular, it does not follow merely from an equality on geometric points.

@[simp]

theorem WeierstrassCurve.additionMorphism_right_unit_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id W.projModel) (CategoryTheory.CategoryStruct.comp W.projModelOver W.projModelZero) ⋯) (CategoryTheory.CategoryStruct.comp W.additionMorphism h) = h

The zero section is a right identity for the Bosma–Lenstra addition morphism on the projective Weierstrass model. This is an equality of scheme morphisms over an arbitrary commutative base ring; in particular, it does not follow merely from an equality on geometric points.

@[simp]

theorem WeierstrassCurve.additionMorphism_left_unit {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp W.projModelOver W.projModelZero) (CategoryTheory.CategoryStruct.id W.projModel) ⋯) W.additionMorphism = CategoryTheory.CategoryStruct.id W.projModel

The zero section is a left identity for the Bosma–Lenstra addition morphism on the projective Weierstrass model, over an arbitrary commutative base ring.

@[simp]

theorem WeierstrassCurve.additionMorphism_left_unit_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp W.projModelOver W.projModelZero) (CategoryTheory.CategoryStruct.id W.projModel) ⋯) (CategoryTheory.CategoryStruct.comp W.additionMorphism h) = h

The zero section is a left identity for the Bosma–Lenstra addition morphism on the projective Weierstrass model, over an arbitrary commutative base ring.