The Bosma–Lenstra addition morphism commutes with changes of variables

Let W be an elliptic Weierstrass curve over a commutative ring R, let C be a change of variables over R, and let S = Spec R. The change of variables induces the isomorphism WeierstrassCurve.projModelVariableChangeIso W C : projModel (C • W) ≅ projModel W over S, which preserves the zero section. This file shows that it also carries the Bosma–Lenstra addition morphism WeierstrassCurve.additionMorphism of C • W to that of W. This is what compares the addition morphisms of two local Weierstrass models of an elliptic curve, once the pointed isomorphism between them is known to be induced by a change of variables.

Over a Noetherian integral domain, the fibre product projModel (C • W) ×_S projModel (C • W) is reduced and projModel W is separated, so the two morphisms are compared on points with values in fields. Such a point is a pair of points with homogeneous coordinates P and Q. The isomorphism sends the point with homogeneous coordinates P to the point with homogeneous coordinates C.toMatrix *ᵥ P, and the addition morphism sends a pair of points to the point with homogeneous coordinates the sum add P Q of Mathlib's addition of point representatives. The two resulting points agree because C.toMatrix *ᵥ add P Q and add (C.toMatrix *ᵥ P) (C.toMatrix *ᵥ Q) are equivalent (WeierstrassCurve.Projective.toMatrix_mulVec_add_equiv).

An elliptic Weierstrass curve W over an arbitrary commutative ring is the base change of one, W₀, over a Noetherian integral domain R₀ (WeierstrassCurve.exists_map_eq_of_isElliptic). Adjoining to R₀ the coefficients u, r, s and t of a universal change of variables, with u inverted, gives a Noetherian integral domain R₁, and the pair (W, C) is the base change of a pair over R₁ (WeierstrassCurve.exists_map_eq_and_map_eq_of_isElliptic). The compatibility passes to base changes, because the addition morphism and the isomorphism induced by a change of variables both commute with base change (WeierstrassCurve.additionMorphism_projModelBaseChange and WeierstrassCurve.projModelVariableChangeIso_hom_projModelBaseChange).

Main results

• WeierstrassCurve.additionMorphism_projModelVariableChangeIso_hom: the addition morphism of C • W followed by the isomorphism projModel (C • W) ≅ projModel W is the isomorphism on both factors followed by the addition morphism of 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.
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.1–2.2.

@[simp]

theorem WeierstrassCurve.additionMorphism_projModelVariableChangeIso_hom {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) [W.IsElliptic] : CategoryTheory.CategoryStruct.comp (C • W).additionMorphism (W.projModelVariableChangeIso C).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (C • W).projModelOver (C • W).projModelOver W.projModelOver W.projModelOver (W.projModelVariableChangeIso C).hom (W.projModelVariableChangeIso C).hom (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) ⋯ ⋯) W.additionMorphism

The addition morphism commutes with changes of variables. Let W be an elliptic Weierstrass curve over R and C a change of variables, and write S = Spec R. The Bosma–Lenstra addition morphism of C • W, followed by the isomorphism projModel (C • W) ≅ projModel W induced by C, is the isomorphism on both factors projModel (C • W) ×_S projModel (C • W) ⟶ projModel W ×_S projModel W, followed by the addition morphism of W.

@[simp]

theorem WeierstrassCurve.additionMorphism_projModelVariableChangeIso_hom_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) [W.IsElliptic] {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp (C • W).additionMorphism (CategoryTheory.CategoryStruct.comp (W.projModelVariableChangeIso C).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (C • W).projModelOver (C • W).projModelOver W.projModelOver W.projModelOver (W.projModelVariableChangeIso C).hom (W.projModelVariableChangeIso C).hom (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp W.additionMorphism h)

The addition morphism commutes with changes of variables. Let W be an elliptic Weierstrass curve over R and C a change of variables, and write S = Spec R. The Bosma–Lenstra addition morphism of C • W, followed by the isomorphism projModel (C • W) ≅ projModel W induced by C, is the isomorphism on both factors projModel (C • W) ×_S projModel (C • W) ⟶ projModel W ×_S projModel W, followed by the addition morphism of W.