The Bosma–Lenstra addition laws over a local ring

Let W' be a Weierstrass curve over a local ring R with residue field k, and let P and Q be solutions of its projective Weierstrass equation whose reductions are nonsingular points of the reduced curve W'_k. The two Bosma–Lenstra addition laws addXYZ and dblAddXYZ do not vanish simultaneously at the reductions of P and Q, so one of the six coordinates of addXYZ P Q and dblAddXYZ P Q is a unit of R. The law owning that coordinate is a unimodular solution S, and it represents the sum at every field-valued specialization at once: for every ring homomorphism f : R →+* K to a field, f ∘ S represents the sum of f ∘ P and f ∘ Q on W'.map f.

This is what makes the group law compatible with reduction modulo a valuation: a single S represents both the sum over the fraction field of a valuation ring and the sum of the reductions over its residue field. No hypothesis on the discriminant is needed, so this applies to the points with nonsingular reduction on a curve with bad reduction. On an elliptic curve over R every unimodular solution has nonsingular reduction.

Main results

• WeierstrassCurve.Projective.exists_isUnimodular_map_equiv_add: over a local ring, the sum of two solutions with nonsingular reduction has a unimodular representative that computes the sum under every ring homomorphism to a field.

References

• W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.

theorem WeierstrassCurve.Projective.exists_isUnimodular_map_equiv_add {R : Type u} [CommRing R] [IsLocalRing R] {W' : Projective R} {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hP₀ : (W'.map (IsLocalRing.residue R)).Nonsingular (⇑(IsLocalRing.residue R) ∘ P)) (hQ₀ : (W'.map (IsLocalRing.residue R)).Nonsingular (⇑(IsLocalRing.residue R) ∘ Q)) : ∃ (S : Fin 3 → R), W'.Equation S ∧ Module.IsUnimodular R S ∧ ∀ {K : Type v} [inst : Field K] (f : R →+* K), ⇑f ∘ S ≈ (W'.map f).add (⇑f ∘ P) (⇑f ∘ Q)

The sum of two points over a local ring. Let P and Q be solutions of the projective Weierstrass equation of W' over a local ring R whose reductions are nonsingular points of the reduced curve. Then there is a unimodular solution S such that, for every ring homomorphism f : R →+* K to a field, f ∘ S represents the sum of f ∘ P and f ∘ Q on W'.map f. One may take for S whichever of the two Bosma–Lenstra addition laws addXYZ P Q and dblAddXYZ P Q has a unit coordinate.