Evaluation of the formal group series of a Weierstrass curve

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

For a Weierstrass curve W over a complete adic local ring O (the standing setting of the vendored p-adic kit), the fixed-point series w and the chord data evaluate at parameters t in the maximal ideal via ChabautyColeman.MvPSeries.eval. This file provides that evaluation layer: the value W.wEval t, its defining Weierstrass fixed-point equation, the factorization w(t) = t³·v(t) with v(t) ≡ 1 mod 𝔪, the uniqueness of solutions of the fixed-point equation in 𝔪, the evaluated chord data (W.slopeEval, W.interceptEval, W.thirdRootEval, W.addEval), and the formal inverse W.negPoint on the 𝔪-points.

theorem IsLocalRing.isUnit_of_sub_one_mem_maximalIdeal {O : Type u_1} [CommRing O] [IsLocalRing O] {u : O} (h : u - 1 ∈ maximalIdeal O) : IsUnit u

An element of 1 + 𝔪 in a local ring is a unit.

def WeierstrassCurve.wPoly {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) (t r : O) : O

The Weierstrass fixed-point polynomial: the right-hand side of the equation w = t³ + a₁tw + a₂t²w + a₃w² + a₄tw² + a₆w³ satisfied by w = w(t).

Equations

• W.wPoly t r = t ^ 3 + W.a₁ * t * r + W.a₂ * t ^ 2 * r + W.a₃ * r ^ 2 + W.a₄ * t * r ^ 2 + W.a₆ * r ^ 3

theorem WeierstrassCurve.eq_of_wPoly_fixed {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) {t r r' : O} (ht : t ∈ IsLocalRing.maximalIdeal O) (hr : r ∈ IsLocalRing.maximalIdeal O) (hr' : r' ∈ IsLocalRing.maximalIdeal O) (h : r = W.wPoly t r) (h' : r' = W.wPoly t r') : r = r'

Solutions in 𝔪 of the Weierstrass fixed-point equation at a parameter t ∈ 𝔪 are unique: the difference of two solutions is contracted by a factor in 𝔪.

theorem WeierstrassCurve.isUnit_chordCoeff {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) {Λ : O} (hΛ : Λ ∈ IsLocalRing.maximalIdeal O) : IsUnit (1 + W.a₂ * Λ + W.a₄ * Λ ^ 2 + W.a₆ * Λ ^ 3)

The leading coefficient 1 + a₂ Λ + a₄ Λ² + a₆ Λ³ of the chord cubic is a unit for Λ in the maximal ideal.

theorem ChabautyColeman.MvPSeries.eval_mem_maximalIdeal_pow {O : Type u_1} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {σ : Type u_2} {z₀ : σ → O} (hz₀ : MvPowerSeries.HasEval z₀) {k : ℕ} (hmem : ∀ (i : σ), z₀ i ∈ IsLocalRing.maximalIdeal O ^ k) (h : MvPowerSeries σ O) (hcc : MvPowerSeries.constantCoeff h ∈ IsLocalRing.maximalIdeal O ^ k) : eval z₀ h ∈ IsLocalRing.maximalIdeal O ^ k

The value at points of 𝔪^k of a series whose constant coefficient lies in 𝔪^k lies in 𝔪^k.

theorem ChabautyColeman.MvPSeries.eval_mem_maximalIdeal_pow_mul {O : Type u_1} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {σ : Type u_2} {z₀ : σ → O} (hz₀ : MvPowerSeries.HasEval z₀) {j c : ℕ} (hmem : ∀ (i : σ), z₀ i ∈ IsLocalRing.maximalIdeal O ^ j) (h : MvPowerSeries σ O) (hcoeff : ∀ (d : σ →₀ ℕ), Finsupp.degree d < c → (MvPowerSeries.coeff d) h = 0) : eval z₀ h ∈ IsLocalRing.maximalIdeal O ^ (c * j)

The value at points of 𝔪^j of a series whose coefficients vanish below total degree c lies in 𝔪^(c·j).

theorem ChabautyColeman.MvPSeries.eval_mem_maximalIdeal_pow_add_mul {O : Type u_1} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {σ : Type u_2} {z₀ : σ → O} (hz₀ : MvPowerSeries.HasEval z₀) {j a c : ℕ} (hmem : ∀ (i : σ), z₀ i ∈ IsLocalRing.maximalIdeal O ^ j) (h : MvPowerSeries σ O) (hcoeff : ∀ (d : σ →₀ ℕ), (MvPowerSeries.coeff d) h ∈ IsLocalRing.maximalIdeal O ^ a) (hlow : ∀ (d : σ →₀ ℕ), Finsupp.degree d < c → (MvPowerSeries.coeff d) h = 0) : eval z₀ h ∈ IsLocalRing.maximalIdeal O ^ (a + c * j)

The value at points of 𝔪^j of a series whose coefficients lie in 𝔪^a and vanish below total degree c lies in 𝔪^(a + c·j).

noncomputable def WeierstrassCurve.wEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t : O) : O

The value of the fixed-point series w at a parameter t.

Equations

• W.wEval t = ChabautyColeman.MvPSeries.eval (fun (x : Unit) => t) W.wSeries

noncomputable def WeierstrassCurve.vEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t : O) : O

The value of the unit-part series v (with w = t³·v) at a parameter t.

Equations

• W.vEval t = ChabautyColeman.MvPSeries.eval (fun (x : Unit) => t) W.vSeries

theorem WeierstrassCurve.wEval_mem {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.wEval t ∈ IsLocalRing.maximalIdeal O

theorem WeierstrassCurve.wEval_eq {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.wEval t = W.wPoly t (W.wEval t)

The value of w satisfies the Weierstrass fixed-point equation.

theorem WeierstrassCurve.wEval_eq_cube_mul {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.wEval t = t ^ 3 * W.vEval t

The factorization w(t) = t³ · v(t) of the value of w.

theorem WeierstrassCurve.vEval_sub_one_mem {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.vEval t - 1 ∈ IsLocalRing.maximalIdeal O

theorem WeierstrassCurve.isUnit_vEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : IsUnit (W.vEval t)

theorem WeierstrassCurve.wEval_ne_zero {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} [IsDomain O] (ht : t ∈ IsLocalRing.maximalIdeal O) (ht0 : t ≠ 0) : W.wEval t ≠ 0

Evaluation of the chord data

The values of u, its inverse, the formal inverse ι, and the two-parameter chord data (slope, intercept, third root, addition series) at parameters in the maximal ideal, with the evaluated forms of their defining identities.

noncomputable def WeierstrassCurve.uEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t : O) : O

The value of the series u = 1 - a₁t - a₃w(t) at a parameter t.

Equations

• W.uEval t = ChabautyColeman.MvPSeries.eval (fun (x : Unit) => t) W.uSeries

noncomputable def WeierstrassCurve.duEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t : O) : O

The value of the inverse of the series u at a parameter t.

Equations

• W.duEval t = ChabautyColeman.MvPSeries.eval (fun (x : Unit) => t) (W.uSeries.invOfUnit 1)

noncomputable def WeierstrassCurve.iotaEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t : O) : O

The value of the formal inverse series ι at a parameter t.

Equations

• W.iotaEval t = ChabautyColeman.MvPSeries.eval (fun (x : Unit) => t) W.inverseSeries

theorem WeierstrassCurve.uEval_eq {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.uEval t = 1 - W.a₁ * t - W.a₃ * W.wEval t

theorem WeierstrassCurve.uEval_mul_duEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.uEval t * W.duEval t = 1

theorem WeierstrassCurve.isUnit_uEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : IsUnit (W.uEval t)

theorem WeierstrassCurve.isUnit_duEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : IsUnit (W.duEval t)

theorem WeierstrassCurve.iotaEval_eq {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.iotaEval t = -(t * W.duEval t)

theorem WeierstrassCurve.iotaEval_mem {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.iotaEval t ∈ IsLocalRing.maximalIdeal O

theorem WeierstrassCurve.iotaEval_ne_zero {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) [IsDomain O] (ht0 : t ≠ 0) : W.iotaEval t ≠ 0

theorem WeierstrassCurve.eq_two_of_iotaEval_self {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) [NoZeroDivisors O] (ht0 : t ≠ 0) (h : t = W.iotaEval t) : W.a₁ * t + W.a₃ * W.wEval t = 2

A nonzero parameter that is its own formal inverse satisfies a₁ t + a₃ w(t) = 2.

theorem WeierstrassCurve.eval_subst_single {O : Type u_1} [CommRing O] [IsLocalRing O] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) {f : PowerSeries O} (hf : PowerSeries.constantCoeff f = 0) (g : PowerSeries O) : ChabautyColeman.MvPSeries.eval (fun (x : Unit) => t) (PowerSeries.subst f g) = ChabautyColeman.MvPSeries.eval (fun (x : Unit) => ChabautyColeman.MvPSeries.eval (fun (x : Unit) => t) f) g

Evaluation of a one-variable substitution is evaluation at the value.

theorem WeierstrassCurve.wEval_iotaEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.wEval (W.iotaEval t) = -(W.wEval t * W.duEval t)

theorem WeierstrassCurve.iotaEval_iotaEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t : O} (ht : t ∈ IsLocalRing.maximalIdeal O) : W.iotaEval (W.iotaEval t) = t

noncomputable def WeierstrassCurve.slopeEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t₁ t₂ : O) : O

The value of the slope series at a pair of parameters.

Equations

• W.slopeEval t₁ t₂ = ChabautyColeman.MvPSeries.eval (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.slopeSeries

noncomputable def WeierstrassCurve.interceptEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t₁ t₂ : O) : O

The value of the intercept series at a pair of parameters.

Equations

• W.interceptEval t₁ t₂ = ChabautyColeman.MvPSeries.eval (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.interceptSeries

noncomputable def WeierstrassCurve.thirdRootEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t₁ t₂ : O) : O

The value of the third-root series at a pair of parameters.

Equations

• W.thirdRootEval t₁ t₂ = ChabautyColeman.MvPSeries.eval (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.thirdRootSeries

noncomputable def WeierstrassCurve.addEval {O : Type u_1} [CommRing O] (W : WeierstrassCurve O) [UniformSpace O] (t₁ t₂ : O) : O

The value of the addition series at a pair of parameters.

Equations

• W.addEval t₁ t₂ = ChabautyColeman.MvPSeries.eval (Sum.elim (fun (x : Unit) => t₁) fun (x : Unit) => t₂) W.addSeries

theorem WeierstrassCurve.slopeEval_mul_sub {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) : W.slopeEval t₁ t₂ * (t₂ - t₁) = W.wEval t₂ - W.wEval t₁

The evaluated slope identity: λ̂·(t₂ - t₁) = w(t₂) - w(t₁).

theorem WeierstrassCurve.interceptEval_eq {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) : W.interceptEval t₁ t₂ = W.wEval t₁ - W.slopeEval t₁ t₂ * t₁

The evaluated intercept identity: ν̂ = w(t₁) - λ̂·t₁.

theorem WeierstrassCurve.slopeEval_mem {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) : W.slopeEval t₁ t₂ ∈ IsLocalRing.maximalIdeal O

theorem WeierstrassCurve.thirdRootEval_mem {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) : W.thirdRootEval t₁ t₂ ∈ IsLocalRing.maximalIdeal O

theorem WeierstrassCurve.thirdRootEval_relation {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) : (1 + W.a₂ * W.slopeEval t₁ t₂ + W.a₄ * W.slopeEval t₁ t₂ ^ 2 + W.a₆ * W.slopeEval t₁ t₂ ^ 3) * (W.thirdRootEval t₁ t₂ + t₁ + t₂) = -(W.a₁ * W.slopeEval t₁ t₂ + W.a₂ * W.interceptEval t₁ t₂ + W.a₃ * W.slopeEval t₁ t₂ ^ 2 + 2 * W.a₄ * W.slopeEval t₁ t₂ * W.interceptEval t₁ t₂ + 3 * W.a₆ * W.slopeEval t₁ t₂ ^ 2 * W.interceptEval t₁ t₂)

The evaluated third-root relation, with the inverse of the cubic's leading coefficient eliminated.

theorem WeierstrassCurve.wEval_thirdRootEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) [IsDomain O] : W.wEval (W.thirdRootEval t₁ t₂) = W.slopeEval t₁ t₂ * W.thirdRootEval t₁ t₂ + W.interceptEval t₁ t₂

The evaluated on-line identity: w(t̂₃) = λ̂·t̂₃ + ν̂.

theorem WeierstrassCurve.addEval_eq {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) : W.addEval t₁ t₂ = W.iotaEval (W.thirdRootEval t₁ t₂)

The evaluated addition series is the formal inverse of the evaluated third root.

theorem WeierstrassCurve.addEval_sub_add_mem {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} {j : ℕ} (hj : j ≠ 0) (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O ^ j) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O ^ j) : W.addEval t₁ t₂ - (t₁ + t₂) ∈ IsLocalRing.maximalIdeal O ^ (2 * j)

The addition series deviates from t₁ + t₂ by 𝔪^(2j) when both parameters lie in 𝔪^j: the formal group law is t₁ + t₂ to first order.

theorem WeierstrassCurve.interceptEval_eq' {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) : W.interceptEval t₁ t₂ = W.wEval t₂ - W.slopeEval t₁ t₂ * t₂

The symmetric evaluated intercept identity: ν̂ = w(t₂) - λ̂·t₂.

@[simp]

theorem WeierstrassCurve.wEval_zero {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] : W.wEval 0 = 0

@[simp]

theorem WeierstrassCurve.iotaEval_zero {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] : W.iotaEval 0 = 0

theorem WeierstrassCurve.thirdRootEval_ne_zero {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ t₂ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) (h₂ : t₂ ∈ IsLocalRing.maximalIdeal O) [IsDomain O] (hx : t₁ * W.wEval t₂ ≠ t₂ * W.wEval t₁) : W.thirdRootEval t₁ t₂ ≠ 0

The third root does not vanish when the two points have distinct x-coordinates (else the chord would be vertical).

theorem WeierstrassCurve.addEval_iotaEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {t₁ : O} (h₁ : t₁ ∈ IsLocalRing.maximalIdeal O) : W.addEval t₁ (W.iotaEval t₁) = 0

The evaluated formal inverse identity: F(t, ι(t)) = 0.

noncomputable def WeierstrassCurve.negPoint {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] (z : W.formalGroupLaw.Points) : W.formalGroupLaw.Points

The formal inverse on the 𝔪-points of the formal group of a Weierstrass curve.

Equations

• W.negPoint z x✝ = ⟨W.iotaEval ↑(z ()), ⋯⟩

@[simp]

theorem WeierstrassCurve.negPoint_apply_coe {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] (z : W.formalGroupLaw.Points) : ↑(W.negPoint z ()) = W.iotaEval ↑(z ())

theorem WeierstrassCurve.add_apply_coe_eq_addEval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] (z z' : W.formalGroupLaw.Points) : ↑((z + z') ()) = W.addEval ↑(z ()) ↑(z' ())

The coordinate of a sum of 𝔪-points is the evaluated addition series.

theorem WeierstrassCurve.nsmul_apply_coe_eq_eval {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] (z : W.formalGroupLaw.Points) (m : ℕ) : ↑((m • z) ()) = ChabautyColeman.MvPSeries.eval (fun (x : Unit) => ↑(z ())) (W.formalGroupLaw.mulSeries m)

The coordinate of an m-fold multiple is the value of the multiplication-by-m series at the parameter.

theorem WeierstrassCurve.nsmul_apply_coe_mem_and_sub_mem {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] {z : W.formalGroupLaw.Points} {k : ℕ} (hk : k ≠ 0) (hz : ↑(z ()) ∈ IsLocalRing.maximalIdeal O ^ k) (m : ℕ) : ↑((m • z) ()) ∈ IsLocalRing.maximalIdeal O ^ k ∧ ↑((m • z) ()) - m • ↑(z ()) ∈ IsLocalRing.maximalIdeal O ^ (2 * k)

First-order congruence for multiples: the parameter of m • z lies in the same 𝔪-power level as the parameter of z and is congruent to m times it modulo the double level.

theorem WeierstrassCurve.add_negPoint {O : Type u_1} [CommRing O] [IsLocalRing O] (W : WeierstrassCurve O) [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] [IsUniformAddGroup O] [CompleteSpace O] [T2Space O] [IsTopologicalRing O] (z : W.formalGroupLaw.Points) : z + W.negPoint z = 0

The formal inverse is a right inverse for the addition of 𝔪-points.