Reduction of points modulo a valuation

Let v be a valuation on a field F, with valuation ring O and residue field k, and let W be a Weierstrass curve over F with an integral model W_O over O. Every point of W(F) reduces to a k-point of the projective plane lying on the reduced curve W_k = W_O ⊗ k: write the point in projective coordinates (X : Y : Z) with X, Y, Z ∈ O not all in the maximal ideal, and reduce the coordinates. This is the reduction map E(K) → E_k(k) of Silverman VII.2, here for an arbitrary valuation and an arbitrary integral model. Throughout, res a denotes the image in k of an element a of O.

The value is a class of Fin 3 → k modulo scaling, Mathlib's WeierstrassCurve.Projective.PointClass. It need not be a nonsingular point: at a point reducing to the singular point of a curve with bad reduction it is not.

Point.reduction is defined by cases rather than through a choice of primitive coordinates. An affine point (x, y) with v(x) ≤ 1 has v(y) ≤ 1 as well, and reduces to (res x : res y : 1); one with 1 < v(x) has v(x) < v(y), so (x : y : 1) = (x / y : 1 : 1 / y) with x / y and 1 / y in the maximal ideal, and it reduces to (0 : 1 : 0). That this agrees with reducing any primitive representative is Point.reduction_some_eq_mk.

Main definitions

• WeierstrassCurve.Affine.Point.reduction: the reduction of a point of W(F).

Main results

• WeierstrassCurve.Affine.Point.reduction_some_eq_mk: the reduction of a point is the reduction of any primitive integral representative of it.
• WeierstrassCurve.Affine.Point.equation_of_reduction_eq: every representative of the reduction lies on the reduced curve.
• WeierstrassCurve.Affine.Point.reduction_eq_zero_iff: a point reduces to (0 : 1 : 0) exactly when it is the point at infinity or its x-coordinate has a pole. This is the set E₁(F), the kernel of reduction.
• WeierstrassCurve.Affine.Point.reduction_neg: reduction commutes with negation.

References

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

noncomputable def WeierstrassCurve.Affine.Point.reduction {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] : W.Point → Projective.PointClass (IsLocalRing.ResidueField ↥v.valuationSubring)

The reduction of a point modulo a valuation, as a point class of the projective plane over the residue field. The point at infinity, and an affine point whose x-coordinate has a pole, reduce to (0 : 1 : 0); an affine point with integral x-coordinate, whose y-coordinate is then integral too, reduces to (res x : res y : 1).

Equations

• One or more equations did not get rendered due to their size.
• WeierstrassCurve.Affine.Point.reduction v WeierstrassCurve.Affine.Point.zero = ⟦![0, 1, 0]⟧

@[simp]

theorem WeierstrassCurve.Affine.Point.reduction_zero {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] : reduction v 0 = ⟦![0, 1, 0]⟧

@[simp]

theorem WeierstrassCurve.Affine.Point.reduction_some_of_valuation_le_one {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] {x y : F} (h : W.Nonsingular x y) (hx : v x ≤ 1) : reduction v (some x y h) = ⟦![(IsLocalRing.residue ↥v.valuationSubring) ⟨x, ⋯⟩, (IsLocalRing.residue ↥v.valuationSubring) ⟨y, ⋯⟩, 1]⟧

A point with integral x-coordinate reduces to the reduction of its coordinates.

@[simp]

theorem WeierstrassCurve.Affine.Point.reduction_some_of_one_lt {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] {x y : F} (h : W.Nonsingular x y) (hx : 1 < v x) : reduction v (some x y h) = ⟦![0, 1, 0]⟧

A point whose x-coordinate has a pole reduces to (0 : 1 : 0).

theorem WeierstrassCurve.Affine.Point.reduction_some_eq_mk {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] {x y : F} (h : W.Nonsingular x y) {X Y Z : ↥v.valuationSubring} (hX : ↑X = x * ↑Z) (hY : ↑Y = y * ↑Z) (hu : IsUnit X ∨ IsUnit Y ∨ IsUnit Z) : reduction v (some x y h) = ⟦![(IsLocalRing.residue ↥v.valuationSubring) X, (IsLocalRing.residue ↥v.valuationSubring) Y, (IsLocalRing.residue ↥v.valuationSubring) Z]⟧

Reduction is computed by any primitive representative. If (X : Y : Z), with coordinates in the valuation ring and at least one of them a unit, represents the affine point (x, y), then the point reduces to (res X : res Y : res Z).

theorem WeierstrassCurve.Affine.Point.reduction_eq_zero_iff {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] (P : W.Point) : reduction v P = ⟦![0, 1, 0]⟧ ↔ P = 0 ∨ 1 < v P.xCoord

The kernel of reduction. A point reduces to (0 : 1 : 0) exactly when it is the point at infinity or its x-coordinate has a pole; these points form E₁(F).

theorem WeierstrassCurve.Affine.Point.equation_of_reduction_eq {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] {P : W.Point} {Q : Fin 3 → IsLocalRing.ResidueField ↥v.valuationSubring} (hQ : reduction v P = ⟦Q⟧) : ((integralModel (↥v.valuationSubring) W).map (IsLocalRing.residue ↥v.valuationSubring)).toProjective.Equation Q

The reduction lies on the reduced curve: every representative of the reduction of a point satisfies the projective equation of the integral model read over the residue field.

@[simp]

theorem WeierstrassCurve.Affine.Point.reduction_neg {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] (P : W.Point) : reduction v (-P) = ((integralModel (↥v.valuationSubring) W).map (IsLocalRing.residue ↥v.valuationSubring)).toProjective.negMap (reduction v P)

Reduction commutes with negation, the negation on the right being that of the reduced curve.