Hensel's lemma for Weierstrass equations

Let R be a Henselian local ring with residue field k, and let W be a Weierstrass curve over R. Every nonsingular point of the reduced curve W_k = W ⊗ k is the residue of a nonsingular point of W. This is Hensel's lemma applied to the Weierstrass equation in whichever variable has a nonvanishing partial derivative at the point of W_k.

The singular point of W_k lifts too, when it is a node at the origin: if a₃, a₄ ∈ 𝔪 and b₂ is a unit, then the two partial derivatives of the Weierstrass polynomial vanish at some (r, t) ∈ 𝔪², and the translation x ↦ x + r, y ↦ y + t makes a₃ = a₄ = 0. The two conditions combine to 6 r² + b₂ r + b₄ = 0, a quadratic with unit linear coefficient b₂, which Hensel's lemma solves; then t is read off from either condition, as 2 or a₁ is a unit. When b₂ is a unit, a root modulo 𝔪 of the tangent quadratic T² + a₁ T − a₂, whose discriminant is b₂, is simple, so it lifts to a root in R: the tangent directions of a split node lift with it.

For a finite residue field and a nonsplit tangent quadratic, a discriminant that is a unit times a square gives a solution with both coordinates in the maximal ideal. The centred case reduces to a residue conic, whose points are obtained from surjectivity of the finite-field norm. In the general case, when a₃ or a₄ is a unit the reduction is nonsingular at the origin, so Hensel's lemma (WeierstrassCurve.Affine.exists_nonsingular_residue_eq at (0, 0)) lifts it to a solution in 𝔪; otherwise the general case follows by the translation above.

Main results

• WeierstrassCurve.Affine.exists_nonsingular_residue_eq: over a Henselian local ring, every nonsingular point of the reduced curve is the residue of a nonsingular point.

• WeierstrassCurve.exists_translate_a₃_eq_zero_and_a₄_eq_zero: over a Henselian local ring, if a₃, a₄ ∈ 𝔪 and b₂ is a unit, a translation by an element of 𝔪² makes a₃ = a₄ = 0.

• WeierstrassCurve.exists_tangentQuadratic_eq_zero: over a Henselian local ring, if b₂ is a unit, a root modulo 𝔪 of the tangent quadratic lifts to a root.

• WeierstrassCurve.associated_a₆_Δ_of_a₃_eq_zero_of_a₄_eq_zero: over a local ring, on a centred node with b₂ a unit, a₆ and Δ are associated.

• WeierstrassCurve.exists_equation_mem_maximalIdeal_of_a₃_eq_zero_of_a₄_eq_zero: the centred nonsplit equation with even discriminant order has a solution in the maximal ideal.

• WeierstrassCurve.exists_equation_mem_maximalIdeal_of_tangentQuadratic_no_roots: the same lifting result for the uncentred equation.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.2.1.
• J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, GTM 151, IV.9.

theorem WeierstrassCurve.Affine.exists_nonsingular_residue_eq {R : Type u_1} [CommRing R] [HenselianLocalRing R] {W : Affine R} {x₀ y₀ : R} (h : (W.map (IsLocalRing.residue R)).Nonsingular ((IsLocalRing.residue R) x₀) ((IsLocalRing.residue R) y₀)) : ∃ (x : R) (y : R), W.Nonsingular x y ∧ (IsLocalRing.residue R) x = (IsLocalRing.residue R) x₀ ∧ (IsLocalRing.residue R) y = (IsLocalRing.residue R) y₀

Nonsingular points lift along a Henselian local ring. Over a Henselian local ring R, every nonsingular point of the reduction of a Weierstrass curve W to the residue field is the residue of a nonsingular point of W.

theorem WeierstrassCurve.exists_translate_a₃_eq_zero_and_a₄_eq_zero {R : Type u_1} [CommRing R] [HenselianLocalRing R] (W : WeierstrassCurve R) (h₃ : W.a₃ ∈ IsLocalRing.maximalIdeal R) (h₄ : W.a₄ ∈ IsLocalRing.maximalIdeal R) (hb₂ : IsUnit W.b₂) : ∃ (r : R) (t : R), r ∈ IsLocalRing.maximalIdeal R ∧ t ∈ IsLocalRing.maximalIdeal R ∧ ({ u := 1, r := r, s := 0, t := t } • W).a₃ = 0 ∧ ({ u := 1, r := r, s := 0, t := t } • W).a₄ = 0

Centring at a singular point of the reduction. Over a Henselian local ring, if a₃ and a₄ lie in the maximal ideal and b₂ is a unit, then for some r, t ∈ 𝔪 the translation x ↦ x + r, y ↦ y + t makes a₃ = a₄ = 0: (r, t) is a critical point of the Weierstrass polynomial.

theorem WeierstrassCurve.exists_tangentQuadratic_eq_zero {R : Type u_1} [CommRing R] [HenselianLocalRing R] (W : WeierstrassCurve R) (hb₂ : IsUnit W.b₂) {t₀ : R} (ht₀ : t₀ ^ 2 + W.a₁ * t₀ - W.a₂ ∈ IsLocalRing.maximalIdeal R) : ∃ (α : R), α ^ 2 + W.a₁ * α - W.a₂ = 0 ∧ α - t₀ ∈ IsLocalRing.maximalIdeal R

The tangent directions of a node lift. Over a Henselian local ring, if b₂ is a unit, a root t₀ modulo the maximal ideal of the tangent quadratic T² + a₁ T − a₂ lifts to a root α with α ≡ t₀. The root is simple: the derivative 2 t₀ + a₁ squares to b₂ modulo the maximal ideal.

theorem WeierstrassCurve.associated_a₆_Δ_of_a₃_eq_zero_of_a₄_eq_zero {R : Type u_1} [CommRing R] [IsLocalRing R] {W : WeierstrassCurve R} (h₃ : W.a₃ = 0) (h₄ : W.a₄ = 0) (h₆ : W.a₆ ∈ IsLocalRing.maximalIdeal R) (hb₂ : IsUnit W.b₂) : Associated W.a₆ W.Δ

On a centred node, a₆ and Δ are associated. Over a local ring, if a₃ = a₄ = 0, a₆ ∈ 𝔪 and b₂ is a unit, then Δ = -a₆ (b₂³ + 432 a₆) with the second factor a unit.

theorem WeierstrassCurve.isUnit_b₂_of_tangentQuadratic_no_roots {R : Type u_1} [CommRing R] [IsLocalRing R] [PerfectField (IsLocalRing.ResidueField R)] (W : WeierstrassCurve R) (hroot : ∀ (t : IsLocalRing.ResidueField R), t ^ 2 + (IsLocalRing.residue R) W.a₁ * t - (IsLocalRing.residue R) W.a₂ ≠ 0) : IsUnit W.b₂

Over a local ring with a perfect residue field, if the tangent quadratic T² + a₁ T − a₂ has no root in the residue field, then b₂ is a unit: otherwise the tangent quadratic has a double root in the perfect residue field.

theorem WeierstrassCurve.exists_equation_mem_maximalIdeal_of_a₃_eq_zero_of_a₄_eq_zero {R : Type u_1} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] (W : WeierstrassCurve R) (h₃ : W.a₃ = 0) (h₄ : W.a₄ = 0) (h₆ : W.a₆ ∈ IsLocalRing.maximalIdeal R) (hroot : ∀ (t : IsLocalRing.ResidueField R), t ^ 2 + (IsLocalRing.residue R) W.a₁ * t - (IsLocalRing.residue R) W.a₂ ≠ 0) {z : R} (hΔ : Associated (z ^ 2) W.Δ) : ∃ (x : R) (y : R), x ∈ IsLocalRing.maximalIdeal R ∧ y ∈ IsLocalRing.maximalIdeal R ∧ W.toAffine.Equation x y

Over a Henselian local ring with finite residue field, suppose a₃ = a₄ = 0, a₆ ∈ 𝔪, and the tangent quadratic has no residue-field root. If the discriminant is associated to a square, the Weierstrass equation has a solution with both coordinates in 𝔪.

theorem WeierstrassCurve.exists_equation_mem_maximalIdeal_of_tangentQuadratic_no_roots {R : Type u_1} [CommRing R] [HenselianLocalRing R] [Finite (IsLocalRing.ResidueField R)] (W : WeierstrassCurve R) (h₆ : W.a₆ ∈ IsLocalRing.maximalIdeal R) (hroot : ∀ (t : IsLocalRing.ResidueField R), t ^ 2 + (IsLocalRing.residue R) W.a₁ * t - (IsLocalRing.residue R) W.a₂ ≠ 0) {z : R} (hΔ : Associated (z ^ 2) W.Δ) : ∃ (x : R) (y : R), x ∈ IsLocalRing.maximalIdeal R ∧ y ∈ IsLocalRing.maximalIdeal R ∧ W.toAffine.Equation x y

A solution in the maximal ideal under a nonsplit tangent quadratic. Over a Henselian local ring with finite residue field, let a₆ ∈ 𝔪 and let the tangent quadratic T² + a₁ T − a₂ have no root in the residue field. When a₃, a₄ ∈ 𝔪 the reduction of W is singular at the origin, a node without rational tangent directions. If Δ is a unit times a square, then some solution (x, y) of W has x, y ∈ 𝔪. This is a converse, for the normal form at the origin, of WeierstrassCurve.exists_associated_sq_Δ_of_isSingular.