Torsion in the formal group when ramification is small relative to p

Let I be an adic ideal of a complete Hausdorff linearly topologised integral domain O. On the group Ê(I) of formal-group parameters of a Weierstrass curve, multiplication by n is evaluation of the multiplication-by-n series [n](T) of the elliptic formal group law. For a prime p that series has the shape [p](T) = p T u(T) + Tᵖ h(T) with u(0) = 1 (FormalGroup.exists_nsmulSeries_eq_of_prime). So if t ∈ I is a nonzero parameter with [p] t = 0, then p u(t) = -t ^ (p - 1) h(t), and u(t) is a unit: p lies in I ^ (p - 1). Contrapositively, Ê(I) has no nonzero p-torsion when p ∉ I ^ (p - 1). This is the case n = 1 of Silverman AEC IV.6.1, which over a discrete valuation ring bounds the valuation of a point of exact order pⁿ by v(p) / (pⁿ - pⁿ⁻¹).

A prime ℓ that is a unit of O never lies in I ^ (ℓ - 1) for a proper ideal I, so the condition only matters for the residue characteristic. Over the completion of a Dedekind domain at a height-one prime u of residue characteristic p, it says that the ramification index of p at u is less than p - 1. Then the kernel of reduction E₁(F_u) is torsion-free; over ℚ this holds at every odd prime. This extends the prime-to-p case (WeierstrassCurve.eq_zero_of_mem_kerReduction_of_nsmul_eq_zero, Silverman AEC VII.3.1) to all of the torsion, which is what makes reduction injective on the whole torsion subgroup at such a prime.

Main results

• WeierstrassCurve.FormalGroupPoint.coe_nsmul: the parameter of n • P is [n] evaluated at the parameter of P.
• WeierstrassCurve.FormalGroupPoint.eq_zero_of_prime_nsmul_eq_zero: Ê(I) has no nonzero p-torsion when p ∉ I ^ (p - 1).
• WeierstrassCurve.FormalGroupPoint.eq_zero_of_nsmul_eq_zero_of_forall_prime_dvd: Ê(I) has no nonzero n-torsion when every prime factor p of n satisfies p ∉ I ^ (p - 1).
• WeierstrassCurve.eq_zero_of_mem_kerReduction_of_nsmul_eq_zero_of_forall_prime_dvd: the kernel of reduction E₁(F_u) has no nonzero n-torsion when every prime factor p of n satisfies p ∉ u ^ (p - 1).

References

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

@[simp]

theorem WeierstrassCurve.FormalGroupPoint.coe_nsmul {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 : ℕ) (P : W.FormalGroupPoint I) : (n • P).val = PowerSeries.eval₂ (RingHom.id O) P.val (W.formalGroup.nsmulSeries n)

Multiplication by n on Ê(I) is evaluation of [n]: the parameter of n • P is the multiplication-by-n series of the elliptic formal group law evaluated at the parameter of P.

theorem WeierstrassCurve.FormalGroupPoint.eq_zero_of_prime_nsmul_eq_zero {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)] [IsDomain O] {p : ℕ} (hp : Nat.Prime p) (hpI : ↑p ∉ I ^ (p - 1)) {P : W.FormalGroupPoint I} (h : p • P = 0) : P = 0

Ê(I) has no p-torsion when p ∉ I ^ (p - 1) (Silverman AEC IV.6.1, for points of order p): over an integral domain, if the prime p does not lie in I ^ (p - 1), the only parameter t ∈ I with p • t = 0 in Ê(I) is t = 0.

theorem WeierstrassCurve.FormalGroupPoint.eq_zero_of_nsmul_eq_zero_of_forall_prime_dvd {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)] [IsDomain O] {n : ℕ} (hn : n ≠ 0) (hnI : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ↑p ∉ I ^ (p - 1)) {P : W.FormalGroupPoint I} (h : n • P = 0) : P = 0

Ê(I) has no n-torsion when every prime factor p of n satisfies p ∉ I ^ (p - 1): over an integral domain, if every prime factor p of n ≠ 0 satisfies p ∉ I ^ (p - 1), the only parameter t ∈ I with n • t = 0 in Ê(I) is t = 0.

theorem WeierstrassCurve.isLinearTopology_adicCompletionIntegers {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.fact_isAdic_maximalIdeal_adicCompletionIntegers {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.eq_zero_of_mem_kerReduction_of_nsmul_eq_zero_of_forall_prime_dvd {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 ≠ 0) (hnu : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ↑p ∉ u.asIdeal ^ (p - 1)) {P : (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).toAffine.Point} (hP : P ∈ kerReduction u C) (h : n • P = 0) : P = 0

The kernel of reduction has no n-torsion when ramification is small relative to the prime factors of n (Silverman AEC IV.6.1 and VII.3.1): a point of E₁(F_u) killed by an integer n ≠ 0 whose prime factors p all satisfy p ∉ u ^ (p - 1) is the point at infinity. When the residue characteristic p has ramification index less than p - 1 at u, as at every odd prime of ℤ, this holds for every n ≠ 0, and E₁(F_u) is torsion-free.