Division by a unit in the elliptic formal group

Multiplication by an integer invertible in the coefficient ring is an automorphism of the elliptic formal group evaluated on an adic ideal. Its inverse is obtained by evaluating the compositional inverse of the multiplication series, whose linear coefficient is that integer. Mathlib's PowerSeries.substInvOfIsUnit supplies this inverse; the existing FormalGroupPoint.coe_nsmul identifies the evaluated multiplication series with scalar multiplication on formal parameters. Consequently the kernel of reduction over a completed discretely valued field is uniquely divisible by integers prime to the residue characteristic. This supplies torsion lifts under good reduction. The point-level theorem WeierstrassCurve.exists_nsmul_eq_of_pole gives division inside the points reducing to infinity for any integral elliptic equation over the completion.

References

• J. Silverman, The Arithmetic of Elliptic Curves, IV.3.2 and VII.3.1.

theorem WeierstrassCurve.FormalGroupPoint.nsmul_surjective {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {W : WeierstrassCurve O} {I : Ideal O} [Fact (IsAdic I)] {n : ℕ} (hn : IsUnit ↑n) : Function.Surjective fun (P : W.FormalGroupPoint I) => n • P

Multiplication by an integer invertible in the coefficient ring is surjective on the formal group evaluated on an adic ideal.

theorem WeierstrassCurve.FormalGroupPoint.nsmul_bijective {O : Type u_1} [CommRing O] [UniformSpace O] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] [IsLinearTopology O O] {W : WeierstrassCurve O} {I : Ideal O} [Fact (IsAdic I)] {n : ℕ} (hn : IsUnit ↑n) : Function.Bijective fun (P : W.FormalGroupPoint I) => n • P

Multiplication by an integer invertible in the coefficient ring is bijective on the formal group evaluated on an adic ideal.

theorem WeierstrassCurve.instIsLinearTopologySubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_tauCeti_4 {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) : IsLinearTopology ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)

theorem WeierstrassCurve.instFactIsAdicSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersMaximalIdeal_tauCeti_4 {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) : Fact (IsAdic (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)))

theorem WeierstrassCurve.nsmul_kerReduction_bijective {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [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] {n : ℕ} (hn : ↑n ∉ u.asIdeal) : Function.Bijective fun (P : ↥(kerReduction u C)) => n • P

The kernel of reduction is uniquely divisible by integers prime to the residue characteristic.

theorem WeierstrassCurve.exists_nsmul_eq_of_pole {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] (u : IsDedekindDomain.HeightOneSpectrum A) (V : WeierstrassCurve (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)) [hV : IsIntegral (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) V] [V.IsElliptic] {n : ℕ} (hn : ↑n ∉ u.asIdeal) {P : V.toAffine.Point} (hP : P = 0 ∨ 1 < Valued.v P.xCoord) : ∃ (Q : V.toAffine.Point), (Q = 0 ∨ 1 < Valued.v Q.xCoord) ∧ n • Q = P

Over a completed discretely valued field, division by an integer prime to the residue characteristic preserves the points reducing to infinity, for any integral elliptic equation.