Reduction of points at good reduction

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 whose discriminant is a unit of O, so that W has good reduction and the reduced curve W_k = W_O ⊗ k is an elliptic curve. This file shows that reduction of points (WeierstrassCurve.Affine.Point.reduction) is then a group homomorphism W(F) →+ W_k(k): Silverman VII.2.1 in the case of good reduction, where the subgroup E₀(F) of points with nonsingular reduction (WeierstrassCurve.Affine.nonsingularReduction) is all of W(F). Its kernel is the kernel of reduction E₁(F), the points whose x-coordinate has a pole, and it is surjective when O is Henselian.

Since the reduced curve is elliptic, every point of it is nonsingular, so every point of W(F) has nonsingular reduction. The reduction homomorphism is then the homomorphism WeierstrassCurve.Affine.nonsingularReductionHom on E₀(F) = W(F).

Main definitions

• WeierstrassCurve.Affine.Point.reductionHom: at good reduction, the reduction homomorphism W(F) →+ W_k(k).

Main results

• WeierstrassCurve.Affine.Point.nonsingularLift_reduction: at good reduction, every point reduces to a nonsingular point of the reduced curve.
• WeierstrassCurve.Affine.nonsingularReduction_eq_top: at good reduction, every point has nonsingular reduction.
• WeierstrassCurve.Affine.Point.reduction_add: at good reduction, reduction commutes with addition.
• WeierstrassCurve.Affine.Point.reductionHom_eq_zero_iff: the kernel of the reduction homomorphism consists of the point at infinity and the points whose x-coordinate has a pole.
• WeierstrassCurve.Affine.Point.reductionHom_surjective: if the valuation ring is Henselian, the reduction homomorphism is surjective.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.2.1.
• W. Bosma and H. W. Lenstra, Jr., Complete systems of two addition laws for elliptic curves, J. Number Theory 53 (1995), 229–240.

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

At good reduction, points reduce to nonsingular points. If the integral model of W has unit discriminant, the reduction of every point of W(F) is a nonsingular point of the reduced curve.

@[simp]

theorem WeierstrassCurve.Affine.nonsingularReduction_eq_top {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] : nonsingularReduction v W = ⊤

At good reduction, every point has nonsingular reduction: E₀(F) = W(F).

@[simp]

theorem WeierstrassCurve.Affine.Point.reduction_add {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] (P Q : W.Point) : reduction v (P + Q) = ((integralModel (↥v.valuationSubring) W).map (IsLocalRing.residue ↥v.valuationSubring)).toProjective.addMap (reduction v P) (reduction v Q)

At good reduction, reduction commutes with addition. If the integral model of W has unit discriminant, the reduction of P + Q is the sum of the reductions of P and Q on the reduced curve.

noncomputable def WeierstrassCurve.Affine.Point.reductionHom {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] [DecidableEq (IsLocalRing.ResidueField ↥v.valuationSubring)] : W.Point →+ ((integralModel (↥v.valuationSubring) W).map (IsLocalRing.residue ↥v.valuationSubring)).toAffine.Point

The reduction homomorphism at good reduction. If the integral model of W has unit discriminant, reduction of points is a group homomorphism W(F) →+ W_k(k) to the points of the reduced curve: a point with integral x-coordinate goes to the residues of its coordinates (reductionHom_some_of_valuation_le_one), and the other points go to the point at infinity. It is the reduction homomorphism WeierstrassCurve.Affine.nonsingularReductionHom on E₀(F) = W(F).

theorem WeierstrassCurve.Affine.Point.reductionHom_apply {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] [DecidableEq (IsLocalRing.ResidueField ↥v.valuationSubring)] (P : W.Point) (hP : P ∈ nonsingularReduction v W) : (reductionHom v) P = (nonsingularReductionHom v W) ⟨P, hP⟩

At good reduction, the reduction homomorphism is the reduction homomorphism on points with nonsingular reduction.

@[simp]

theorem WeierstrassCurve.Affine.Point.reductionHom_toProjective_point {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] [DecidableEq (IsLocalRing.ResidueField ↥v.valuationSubring)] (P : W.Point) : ((reductionHom v) P).toProjective.point = reduction v P

The reduction homomorphism, read in projective coordinates, is the reduction of points.

theorem WeierstrassCurve.Affine.Point.reductionHom_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] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] [DecidableEq (IsLocalRing.ResidueField ↥v.valuationSubring)] {x y : F} (h : W.Nonsingular x y) (hx : v x ≤ 1) (h' : ((integralModel (↥v.valuationSubring) W).map (IsLocalRing.residue ↥v.valuationSubring)).toAffine.Nonsingular ((IsLocalRing.residue ↥v.valuationSubring) ⟨x, ⋯⟩) ((IsLocalRing.residue ↥v.valuationSubring) ⟨y, ⋯⟩)) : (reductionHom v) (some x y h) = some ((IsLocalRing.residue ↥v.valuationSubring) ⟨x, ⋯⟩) ((IsLocalRing.residue ↥v.valuationSubring) ⟨y, ⋯⟩) h'

At good reduction, a point with integral x-coordinate reduces to the residues of its coordinates.

theorem WeierstrassCurve.Affine.Point.reductionHom_eq_zero_iff {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] [DecidableEq (IsLocalRing.ResidueField ↥v.valuationSubring)] (P : W.Point) : (reductionHom v) P = 0 ↔ P = 0 ∨ 1 < v P.xCoord

The kernel of reduction at good reduction: a point reduces to the point at infinity exactly when it is the point at infinity or its x-coordinate has a pole.

@[simp]

theorem WeierstrassCurve.Affine.Point.reductionHom_some_of_one_lt {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] [DecidableEq (IsLocalRing.ResidueField ↥v.valuationSubring)] {x y : F} (h : W.Nonsingular x y) (hx : 1 < v x) : (reductionHom v) (some x y h) = 0

At good reduction, a point whose x-coordinate has a pole reduces to the point at infinity.

theorem WeierstrassCurve.Affine.Point.reductionHom_surjective {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [(integralModel (↥v.valuationSubring) W).IsElliptic] [DecidableEq F] [DecidableEq (IsLocalRing.ResidueField ↥v.valuationSubring)] [HenselianLocalRing ↥v.valuationSubring] : Function.Surjective ⇑(reductionHom v)

Reduction is onto at good reduction when the valuation ring is Henselian, for instance complete: every point of the reduced elliptic curve is the reduction of a point of W(F).