The point-level reduction map over the completion

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

For a good integral model W₀ of W over 𝒪_v (good reduction: [W₀.IsElliptic]), the reduction map E(K_v) → E_red(k_v) sends a point with integral coordinates to their residues and a point of the kernel of reduction (a pole at x) to the point at infinity.

This file is the completion-level engine behind reduction at a prime of a Dedekind domain R with fraction field K: the user-facing API red/redHom : E(K) →+ E_red(R ⧸ v.asIdeal) lives in EllipticCurves.ReductionAtPrime, which identifies it with the maps built here along the base change E(K) → E(K_v).

Main definitions and statements

• WeierstrassCurve.Affine.adicRed, WeierstrassCurve.Affine.adicRedHom: the reduction map/homomorphism E(K_v) →+ E_red(k_v).
• WeierstrassCurve.Affine.adicRed_eq_zero_iff: the kernel of adicRed is the filtration step E₁(K_v).
• WeierstrassCurve.Affine.sub_mem_filtration_of_red_eq: the congruence criterion — two points with equal reduction differ by an element of E₁(K_v).
• WeierstrassCurve.Affine.eq_zero_of_isOfFinAddOrder_of_adicRed_eq_zero, WeierstrassCurve.Affine.addOrderOf_adicRed: adicRed is injective on torsion and preserves the additive order of a torsion point, under the standard ramification condition on the residue characteristic.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Affine.adicRedCurve {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) : Affine (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))

The reduction E_red of the integral model W₀ modulo the maximal ideal, a Weierstrass curve over the residue field k_v; under good reduction ([W₀.IsElliptic], assumed for all results below about adicRed) it is again elliptic.

Equations

• WeierstrassCurve.Affine.adicRedCurve W₀ = (W₀.map (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))).toAffine

theorem WeierstrassCurve.Affine.equation_integral {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) {x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (h : W.Equation x y) (hx : Valued.v x ≤ 1) (hy : Valued.v y ≤ 1) : W₀.toAffine.Equation ⟨x, hx⟩ ⟨y, hy⟩

An integral solution of the Weierstrass equation over K_v is a solution over 𝒪_v.

theorem WeierstrassCurve.Affine.nonsingular_deriv_disj {F : Type u_3} [Field F] {E' : Affine F} {a b : F} (h : E'.Nonsingular a b) : E'.a₁ * b - (3 * a ^ 2 + 2 * E'.a₂ * a + E'.a₄) ≠ 0 ∨ b - E'.negY a b ≠ 0

At a nonsingular point of a Weierstrass curve, one of the two partial derivatives of the Weierstrass polynomial is nonzero.

theorem WeierstrassCurve.Affine.red_slope {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))] {x₁ x₂ y₁ y₂ : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (hx₁ : Valued.v x₁ ≤ 1) (hx₂ : Valued.v x₂ ≤ 1) (hy₁ : Valued.v y₁ ≤ 1) (hy₂ : Valued.v y₂ ≤ 1) (hc₁ : W.Equation x₁ y₁) (hc₂ : W.Equation x₂ y₂) (hℓ : Valued.v (W.slope x₁ x₂ y₁ y₂) ≤ 1) (hne : ¬((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x₁, hx₁⟩ = (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x₂, hx₂⟩ ∧ (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨y₁, hy₁⟩ = (adicRedCurve W₀).negY ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x₂, hx₂⟩) ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨y₂, hy₂⟩))) : (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨W.slope x₁ x₂ y₁ y₂, ⋯⟩ = (adicRedCurve W₀).slope ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x₁, ⋯⟩) ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x₂, ⋯⟩) ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨y₁, ⋯⟩) ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨y₂, ⋯⟩)

Reduction commutes with the chord/tangent slope, off the reduced anti-diagonal. Mathlib's map_slope cannot apply (the residue map is not an injective field hom), so the secant/tangent branch is chosen by the reduced points: the finite-difference identity turns a K_v-secant that reduces to a tangent into a genuine tangent downstairs.

theorem WeierstrassCurve.Affine.valued_slope_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] {x₁ x₂ y₁ y₂ : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (hx₁ : Valued.v x₁ ≤ 1) (hx₂ : Valued.v x₂ ≤ 1) (hy₁ : Valued.v y₁ ≤ 1) (hy₂ : Valued.v y₂ ≤ 1) (hc₁ : W.Equation x₁ y₁) (hc₂ : W.Equation x₂ y₂) (hne : ¬((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x₁, hx₁⟩ = (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x₂, hx₂⟩ ∧ (IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨y₁, hy₁⟩ = (adicRedCurve W₀).negY ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x₂, hx₂⟩) ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨y₂, hy₂⟩))) : Valued.v (W.slope x₁ x₂ y₁ y₂) ≤ 1

Off the reduced anti-diagonal, the chord/tangent slope of two integral points is integral.

theorem WeierstrassCurve.Affine.adicRed_nonsingular {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] {x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (h : W.Equation x y) (hx : Valued.v x ≤ 1) (hy : Valued.v y ≤ 1) : (adicRedCurve W₀).Nonsingular ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x, hx⟩) ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨y, hy⟩)

The reduced coordinates of an integral point are nonsingular on the smooth curve E_red.

noncomputable def WeierstrassCurve.Affine.adicRed {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] : W.Point → (adicRedCurve W₀).Point

The point-level reduction map. 0 ↦ 0; an affine point with a pole of order ≥ 2 at x (the kernel of reduction) ↦ 0; otherwise the coordinatewise reduction.

Equations

• One or more equations did not get rendered due to their size.
• WeierstrassCurve.Affine.adicRed hW WeierstrassCurve.Affine.Point.zero = 0

@[simp]

theorem WeierstrassCurve.Affine.adicRed_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] : adicRed hW 0 = 0

theorem WeierstrassCurve.Affine.adicRed_some_of_mem {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] {x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} {h : W.Nonsingular x y} (hx : WithZero.exp 2 ≤ Valued.v x) : adicRed hW (Point.some x y h) = 0

Unfolding lemma for adicRed on a kernel point.

theorem WeierstrassCurve.Affine.adicRed_some_of_not_mem {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] {x y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} {h : W.Nonsingular x y} (hx : ¬WithZero.exp 2 ≤ Valued.v x) : adicRed hW (Point.some x y h) = Point.some ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨x, ⋯⟩) ((IsLocalRing.residue ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ⟨y, ⋯⟩) ⋯

Unfolding lemma for adicRed on an integral (non-kernel) point.

theorem WeierstrassCurve.Affine.adicRed_neg {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] (P : W.Point) : adicRed hW (-P) = -adicRed hW P

adicRed commutes with negation.

theorem WeierstrassCurve.Affine.adicRed_eq_zero_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] {P : W.Point} : adicRed hW P = 0 ↔ P ∈ filtration hW 0

The kernel of adicRed is exactly the kernel of reduction E₁(K_v) = filtration hW 0.

theorem WeierstrassCurve.Affine.sub_mem_filtration_of_red_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] {P Q : W.Point} (hPQ : adicRed hW P = adicRed hW Q) : P - Q ∈ filtration hW 0

Congruence criterion: equal reductions of two points differ by a kernel-of-reduction element.

theorem WeierstrassCurve.Affine.eq_zero_of_isOfFinAddOrder_of_adicRed_eq_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] {p : ℕ} (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (hpram : ↑p ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ (p - 1)) {P : W.Point} (hP : IsOfFinAddOrder P) (h0 : adicRed hW P = 0) : P = 0

adicRed is injective on torsion: a torsion point in the kernel of reduction is zero.

theorem WeierstrassCurve.Affine.adicRed_add {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))] (P Q : W.Point) : adicRed hW (P + Q) = adicRed hW P + adicRed hW Q

adicRed is additive.

noncomputable def WeierstrassCurve.Affine.adicRedHom {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))] : W.Point →+ (adicRedCurve W₀).Point

The reduction homomorphism E(K_v) →+ E_red(k_v) over the completion. For the reduction homomorphism over the global field, see redHom in EllipticCurves.ReductionAtPrime.

Equations

• WeierstrassCurve.Affine.adicRedHom hW = AddMonoidHom.mk' (WeierstrassCurve.Affine.adicRed hW) ⋯

@[simp]

theorem WeierstrassCurve.Affine.coe_adicRedHom {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))] : ⇑(adicRedHom hW) = adicRed hW

theorem WeierstrassCurve.Affine.nsmul_eq_zero_of_adicRed_nsmul_eq_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))] {p : ℕ} (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (hpram : ↑p ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ (p - 1)) {P : W.Point} (hP : IsOfFinAddOrder P) {m : ℕ} (h : m • adicRed hW P = 0) : m • P = 0

If a torsion point's reduction is annihilated by m, then so is the point itself.

theorem WeierstrassCurve.Affine.addOrderOf_adicRed {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {W : Affine (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (hW : W₀.map (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = W) [W₀.IsElliptic] [WeierstrassCurve.IsElliptic W] [DecidableEq (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)] [CharZero K] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))] {p : ℕ} (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (hpram : ↑p ∉ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ^ (p - 1)) {P : W.Point} (hP : IsOfFinAddOrder P) : addOrderOf (adicRed hW P) = addOrderOf P

adicRed preserves the additive order of a torsion point (it is injective on torsion, so no collapse of order can occur).