Formal points over a Dedekind adic completion

For a Weierstrass curve over the ring of integers O_v in the completion of a Dedekind domain at a height-one prime, the maximal ideal has enough auxiliary parameters to apply the generic formal point homomorphism construction. This file packages the resulting unconditional additive and injective map from the formal group on that maximal ideal into the points over the completion. It is the discrete adic-completion specialization; the generic construction, conditional on the existence of auxiliary parameters, is in Point.Hom.

Main definitions

• WeierstrassCurve.formalPointHomAdicCompletion: the additive homomorphism from formal-group parameters in the maximal ideal of O_v to points over the completion.

Main results

• WeierstrassCurve.formalPoint_add_adicCompletion: the parametrisation preserves addition.
• WeierstrassCurve.formalPointHomAdicCompletion_injective: the 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.instIsLinearTopologySubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_tauCeti {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsLinearTopology ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem WeierstrassCurve.instFactIsAdicSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersMaximalIdeal_tauCeti {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : Fact (IsAdic (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)))

instance WeierstrassCurve.isIntegral_baseChange_adicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (W : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) : IsIntegral (↥Valued.v.valuationSubring) (W.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

A curve over the completed valuation ring is an integral model of its base change to the completion.

@[simp]

theorem WeierstrassCurve.formalPoint_add_adicCompletion {A : Type u_3} [CommRing A] [IsDedekindDomain A] {F : Type u_4} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [(C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).IsElliptic] (P Q : C.FormalGroupPoint (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u))) : C.formalPoint ⋯ ⋯ = C.formalPoint ⋯ ⋯ + C.formalPoint ⋯ ⋯

The formal parametrisation preserves addition in an adic completion.

noncomputable def WeierstrassCurve.formalPointHomAdicCompletion {A : Type u_3} [CommRing A] [IsDedekindDomain A] {F : Type u_4} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [(C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).IsElliptic] : C.FormalGroupPoint (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) →+ (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).toAffine.Point

The formal parameter map for an adic completion, as an additive homomorphism.

Equations

• WeierstrassCurve.formalPointHomAdicCompletion u C = WeierstrassCurve.formalPointHom (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) C ⋯

@[simp]

theorem WeierstrassCurve.formalPointHomAdicCompletion_apply {A : Type u_3} [CommRing A] [IsDedekindDomain A] {F : Type u_4} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [(C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).IsElliptic] (P : C.FormalGroupPoint (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u))) : (formalPointHomAdicCompletion u C) P = C.formalPoint ⋯ ⋯

The adic-completion formal point homomorphism evaluates to the usual parametrisation.

theorem WeierstrassCurve.formalPointHomAdicCompletion_injective {A : Type u_3} [CommRing A] [IsDedekindDomain A] {F : Type u_4} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (C : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) [(C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).IsElliptic] : Function.Injective ⇑(formalPointHomAdicCompletion u C)

The adic-completion formal point homomorphism is injective.