The formal parameter map is additive

For an adic ideal I of a complete ring O mapping injectively to a field K, the Weierstrass formal group law makes its elements into WeierstrassCurve.FormalGroupPoint W I. The usual parametrisation sends zero to the point at infinity and, for a nonzero parameter, is given by

t ↦ (t / w(t), -1 / w(t))

This file proves that this map is an additive homomorphism into the points of the base-changed curve whenever every parameter distinct from its inverse admits an auxiliary parameter distinct from it, its inverse, and its own inverse.

Main definitions

• WeierstrassCurve.formalPointHom: the additive homomorphism from formal-group parameters in an adic ideal to points of the curve over a field.

Main results

• WeierstrassCurve.formalPoint_add: the parametrisation preserves addition when auxiliary parameters exist.
• WeierstrassCurve.formalPointHom_injective: the resulting homomorphism is injective.

References

• J. Silverman, The Arithmetic of Elliptic Curves, IV.1 and VII.2.

Provenance

Adapted from Michael Stoll's elliptic-curve development (github.com/MichaelStollBayreuth/EllipticCurves @ 66889eada51a, Apache-2.0), files EllipticCurves/WeierstrassFormalGroup/Foundations.lean and EllipticCurves/WeierstrassFormalGroup/Filtration.lean, declarations exists_aux_param, exists_aux_point, formalPoint_add_self and formalPoint_add. The source works with its own multivariable formal-group points; here the argument is rebased onto WeierstrassCurve.FormalGroupPoint and the one-dimensional formal-group API already in Mathlib and Tau Ceti.

theorem WeierstrassCurve.formalPoint_add {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {S : Type u_2} [Field S] [Algebra O S] [FaithfulSMul O S] (I : Ideal O) [Fact (IsAdic I)] (E : WeierstrassCurve O) [(E.baseChange S).IsElliptic] (haux : ∀ (P : E.FormalGroupPoint I), P ≠ -P → ∃ (U : E.FormalGroupPoint I), U ≠ P ∧ U ≠ -P ∧ U ≠ -U) (P Q : E.FormalGroupPoint I) : E.formalPoint ⋯ ⋯ = E.formalPoint ⋯ ⋯ + E.formalPoint ⋯ ⋯

The formal parametrisation preserves addition whenever every parameter distinct from its inverse has an auxiliary parameter distinct from it, its inverse, and the auxiliary parameter's own inverse.

noncomputable def WeierstrassCurve.formalPointHom {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {S : Type u_2} [Field S] [Algebra O S] [FaithfulSMul O S] (I : Ideal O) [Fact (IsAdic I)] (E : WeierstrassCurve O) [(E.baseChange S).IsElliptic] (haux : ∀ (P : E.FormalGroupPoint I), P ≠ -P → ∃ (U : E.FormalGroupPoint I), U ≠ P ∧ U ≠ -P ∧ U ≠ -U) : E.FormalGroupPoint I →+ (E.baseChange S).toAffine.Point

The formal parameter map into the curve's points, as an additive homomorphism whenever the required auxiliary parameters exist.

Equations

• WeierstrassCurve.formalPointHom I E haux = { toFun := WeierstrassCurve.formalPointMap✝ I E, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem WeierstrassCurve.formalPointHom_apply {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {S : Type u_2} [Field S] [Algebra O S] [FaithfulSMul O S] (I : Ideal O) [Fact (IsAdic I)] (E : WeierstrassCurve O) [(E.baseChange S).IsElliptic] (haux : ∀ (P : E.FormalGroupPoint I), P ≠ -P → ∃ (U : E.FormalGroupPoint I), U ≠ P ∧ U ≠ -P ∧ U ≠ -U) (P : E.FormalGroupPoint I) : (formalPointHom I E haux) P = E.formalPoint ⋯ ⋯

The formal point homomorphism evaluates to the usual formal parametrisation.

theorem WeierstrassCurve.formalPointHom_injective {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {S : Type u_2} [Field S] [Algebra O S] [FaithfulSMul O S] (I : Ideal O) [Fact (IsAdic I)] (E : WeierstrassCurve O) [(E.baseChange S).IsElliptic] (haux : ∀ (P : E.FormalGroupPoint I), P ≠ -P → ∃ (U : E.FormalGroupPoint I), U ≠ P ∧ U ≠ -P ∧ U ≠ -U) : Function.Injective ⇑(formalPointHom I E haux)

The formal point homomorphism is injective.