The formal group is the kernel of reduction

Let A be a Dedekind domain with fraction field F, let u be a height-one prime of A, and let C be a Weierstrass curve over the completed valuation ring O_u which is elliptic over the completion F_u. The points of C over F_u reduce modulo u (Point.reduction), and the points reducing to (0 : 1 : 0) form the kernel of reduction E₁(F_u). This file makes that set a subgroup and identifies it with the group Ê(𝔪_u) of formal-group parameters in the maximal ideal: Silverman AEC VII.2.2.

Main definitions

• WeierstrassCurve.kerReduction: the kernel of reduction E₁(F_u), as a subgroup of the points of C over F_u.
• WeierstrassCurve.formalPointAddEquivKerReduction: the isomorphism Ê(𝔪_u) ≃+ E₁(F_u).

Main results

• WeierstrassCurve.range_formalPointHomAdicCompletion_eq_kerReduction: the image of the formal parametrisation is the kernel of reduction.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.2.2.

theorem WeierstrassCurve.instIsLinearTopologySubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_tauCeti_2 {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_2 {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)))

noncomputable def WeierstrassCurve.kerReduction {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] : AddSubgroup (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).toAffine.Point

The kernel of reduction E₁(F_u): the points of C over the completion F_u that reduce to (0 : 1 : 0) modulo u.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.mem_kerReduction_iff {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] {P : (C.baseChange (IsDedekindDomain.HeightOneSpectrum.adicCompletion F u)).toAffine.Point} : P ∈ kerReduction u C ↔ Affine.Point.reduction Valued.v P = ⟦![0, 1, 0]⟧

theorem WeierstrassCurve.range_formalPointHomAdicCompletion_eq_kerReduction {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] : (formalPointHomAdicCompletion u C).range = kerReduction u C

The image of the formal parametrisation is the kernel of reduction.

noncomputable def WeierstrassCurve.formalPointAddEquivKerReduction {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] : C.FormalGroupPoint (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u)) ≃+ ↥(kerReduction u C)

The formal group is the kernel of reduction, Silverman AEC VII.2.2: the formal parametrisation t ↦ (t / w(t), -1 / w(t)) is an isomorphism from the group Ê(𝔪_u) of formal-group parameters in the maximal ideal onto the kernel of reduction E₁(F_u).

Equations

• WeierstrassCurve.formalPointAddEquivKerReduction u C = (AddMonoidHom.ofInjective ⋯).trans (AddEquiv.addSubgroupCongr ⋯)

@[simp]

theorem WeierstrassCurve.coe_formalPointAddEquivKerReduction_apply {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] (P : C.FormalGroupPoint (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F u))) : ↑((formalPointAddEquivKerReduction u C) P) = (formalPointHomAdicCompletion u C) P