Torsion of order prime to the residue characteristic in the formal group

Let I be an adic ideal of a complete Hausdorff linearly topologised ring O. To first order the Weierstrass formal group law is addition, so multiplication by n on the group Ê(I) of formal-group parameters is multiplication by n to first order: if t ∈ I ^ k, then [n] t ≡ n t (mod I ^ (2 k)). When n is a unit of O, a nonzero parameter t therefore cannot satisfy [n] t = 0: from t ∈ I ^ k one gets n t ∈ I ^ (2 k), so t ∈ I ^ (k + 1), and t lies in every power of I, which meet in 0. This is Silverman AEC IV.3.2(b).

Through the identification Ê(𝔪_u) ≃ E₁(F_u) of the formal group with the kernel of reduction over the completion of a Dedekind domain at a height-one prime u, it follows that E₁(F_u) has no nonzero point of order n for any n outside u: the reduction modulo u of a nonzero point of order prime to the residue characteristic is not the point at infinity. This is the kernel half of the injectivity of reduction on prime-to-p torsion (Silverman AEC VII.3.1).

Main results

• WeierstrassCurve.FormalGroupPoint.coe_nsmul_sub_natCast_mul_mem: [n] t ≡ n t (mod I ^ (2 k)) for a parameter t ∈ I ^ k.
• WeierstrassCurve.FormalGroupPoint.eq_zero_of_nsmul_eq_zero: Ê(I) has no nonzero n-torsion when n is a unit of O.
• WeierstrassCurve.eq_zero_of_mem_kerReduction_of_nsmul_eq_zero: the kernel of reduction E₁(F_u) has no nonzero n-torsion when n ∉ u.
• WeierstrassCurve.valuation_xCoord_le_one_and_valuation_yCoord_le_one_of_nsmul_eq_zero: so a nonzero point of E(F_u) of order prime to u has integral coordinates.

References

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

theorem WeierstrassCurve.FormalGroupPoint.coe_nsmul_sub_natCast_mul_mem {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)] {k : ℕ} {P : W.FormalGroupPoint I} (hP : P.val ∈ I ^ k) (n : ℕ) : (n • P).val - ↑n * P.val ∈ I ^ (2 * k)

Multiplication by n on the formal group is multiplication by n to first order: for a parameter t ∈ I ^ k, the parameter of n • t agrees with n * t modulo I ^ (2 * k).

theorem WeierstrassCurve.FormalGroupPoint.eq_zero_of_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)] {n : ℕ} (hn : IsUnit ↑n) {P : W.FormalGroupPoint I} (h : n • P = 0) : P = 0

The formal group has no torsion of unit order (Silverman AEC IV.3.2(b)): if n is a unit of O, the only parameter t ∈ I with n • t = 0 in Ê(I) is t = 0.

theorem WeierstrassCurve.instIsLinearTopologySubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_tauCeti_3 {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_3 {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 {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) {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 torsion prime to the residue characteristic (Silverman AEC VII.3.1): a point of E₁(F_u) killed by an integer n ∉ u is the point at infinity.

theorem WeierstrassCurve.valuation_xCoord_le_one_and_valuation_yCoord_le_one_of_nsmul_eq_zero {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) {P : (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).toAffine.Point} (hP : P ≠ 0) (h : n • P = 0) : Valued.v P.xCoord ≤ 1 ∧ Valued.v P.yCoord ≤ 1

Torsion of order prime to the residue characteristic is integral: a nonzero point of E(F_u) killed by an integer n ∉ u does not lie in the kernel of reduction, so both of its coordinates are integral at u.