The singular points of a Weierstrass model

A Weierstrass model has at most one singular point. This file introduces the predicate for it and proves that uniqueness, over any reduced commutative ring.

Singularity is taken to be the Jacobian criterion: the equation and both of its formal partial derivatives vanish. That is what makes sense over an arbitrary commutative ring, and over a field it is Mathlib's condition, whose Nonsingular carries the note that it "is only mathematically accurate for fields".

Over a general commutative ring uniqueness is not available, but the cube of the difference of the x-coordinates and the fourth power of the difference of the y-coordinates vanish, so the two points differ by a nilpotent in each coordinate; reducedness is exactly what turns that into equality. Every statement here holds in any characteristic, including two and three.

Main definitions

• WeierstrassCurve.Affine.IsSingular: the equation and both formal partials vanish at a point.

Main results

• WeierstrassCurve.Affine.isSingular_iff' and WeierstrassCurve.Affine.isSingular_iff: the coefficient-level restatements, the second as the two equalities Nonsingular negates.
• WeierstrassCurve.Affine.isSingular_zero: singularity at the origin is a₃ = a₄ = a₆ = 0.
• WeierstrassCurve.Affine.equation_iff_of_isSingular: the equation expanded at a singular point (x₁, y₁) has no constant or linear terms.
• WeierstrassCurve.Affine.equation_iff_of_isSingular_zero: so the equation of a model singular at the origin is y² + a₁ x y = x³ + a₂ x².
• WeierstrassCurve.Affine.c₄_eq_b₂_sq_of_isSingular_zero: at such a model, c₄ = b₂².
• WeierstrassCurve.Affine.isSingular_iff_variableChange: singularity at a point is singularity at the origin of the model translated there.
• WeierstrassCurve.Affine.isSingular_iff_equation_and_not_nonsingular: the comparison with Mathlib's Nonsingular.
• WeierstrassCurve.Affine.IsSingular.map, map_isSingular, IsSingular.baseChange and baseChange_isSingular: singularity is carried along a coefficient map or a base change, and reflected by an injective one.
• WeierstrassCurve.Affine.exists_isSingular_of_Δ_eq_zero: over a perfect field, vanishing of the discriminant produces a rational singular point.
• WeierstrassCurve.Affine.Δ_eq_zero_iff_exists_isSingular: the resulting characterization of singular Weierstrass models over a perfect field.
• WeierstrassCurve.Affine.pow_sub_eq_zero_of_isSingular_of_isSingular: two singular points satisfy (x₂ - x₁) ^ 3 = 0 and (y₂ - y₁) ^ 4 = 0.
• WeierstrassCurve.Affine.isNilpotent_sub_of_isSingular_of_isSingular: so each coordinate difference is nilpotent.
• WeierstrassCurve.Affine.subsingleton_singular: over a reduced ring they coincide, so a Weierstrass model has at most one singular point.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.1.

def WeierstrassCurve.Affine.IsSingular {R : Type u_1} [CommRing R] (W : Affine R) (x y : R) : Prop

A point of a Weierstrass model where the equation and both formal partial derivatives vanish — the Jacobian criterion for singularity, which makes sense over any commutative ring.

Over a field this is W.Equation x y ∧ ¬ W.Nonsingular x y, recorded as isSingular_iff_equation_and_not_nonsingular. It is stated separately because Mathlib's Nonsingular carries the note that it "is only mathematically accurate for fields", so over a general ring the three vanishing conditions are what one can actually say.

Equations

• W.IsSingular x y = (W.Equation x y ∧ Polynomial.evalEval x y W.polynomialX = 0 ∧ Polynomial.evalEval x y W.polynomialY = 0)

theorem WeierstrassCurve.Affine.isSingular_iff' {R : Type u_1} [CommRing R] (W : Affine R) (x y : R) : W.IsSingular x y ↔ W.Equation x y ∧ W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) = 0 ∧ 2 * y + W.a₁ * x + W.a₃ = 0

The coefficient-level form of the Jacobian criterion.

theorem WeierstrassCurve.Affine.isSingular_iff {R : Type u_1} [CommRing R] (W : Affine R) (x y : R) : W.IsSingular x y ↔ W.Equation x y ∧ W.a₁ * y = 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∧ y = -y - W.a₁ * x - W.a₃

The Jacobian criterion as two equalities, the form Nonsingular negates.

@[simp]

theorem WeierstrassCurve.Affine.isSingular_zero {R : Type u_1} [CommRing R] (W : Affine R) : W.IsSingular 0 0 ↔ W.a₆ = 0 ∧ W.a₄ = 0 ∧ W.a₃ = 0

A Weierstrass model is singular at the origin exactly when a₃, a₄ and a₆ vanish, so its equation reads y (y + a₁x) = x² (x + a₂).

theorem WeierstrassCurve.Affine.equation_iff_of_isSingular {R : Type u_1} [CommRing R] {W : Affine R} {x₁ y₁ : R} (h : W.IsSingular x₁ y₁) (x y : R) : W.Equation x y ↔ (y - y₁) ^ 2 + W.a₁ * (x - x₁) * (y - y₁) = (x - x₁) ^ 3 + (3 * x₁ + W.a₂) * (x - x₁) ^ 2

The equation expanded at a singular point: at a singular point (x₁, y₁) the constant and linear terms of the equation vanish, so it reads (y - y₁)² + a₁ (x - x₁) (y - y₁) = (x - x₁)³ + (3 x₁ + a₂) (x - x₁)².

theorem WeierstrassCurve.Affine.equation_iff_of_isSingular_zero {R : Type u_1} [CommRing R] {W : Affine R} (h : W.IsSingular 0 0) (x y : R) : W.Equation x y ↔ y ^ 2 + W.a₁ * x * y = x ^ 3 + W.a₂ * x ^ 2

At a model singular at the origin the equation reads y² + a₁ x y = x³ + a₂ x².

theorem WeierstrassCurve.Affine.c₄_eq_b₂_sq_of_isSingular_zero {R : Type u_1} [CommRing R] {W : Affine R} (h : W.IsSingular 0 0) : c₄ W = b₂ W ^ 2

For a model singular at the origin, c₄ is the square of b₂, the discriminant of the tangent quadratic T² + a₁ T - a₂.

theorem WeierstrassCurve.Affine.isSingular_iff_equation_and_not_nonsingular {R : Type u_1} [CommRing R] {W : Affine R} {x y : R} : W.IsSingular x y ↔ W.Equation x y ∧ ¬W.Nonsingular x y

The Jacobian criterion is Mathlib's singularity condition, Nonsingular being the conjunction of the equation with the negation of both partials vanishing.

theorem WeierstrassCurve.Affine.isSingular_iff_variableChange {R : Type u_1} [CommRing R] (W : Affine R) (x y : R) : W.IsSingular x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).IsSingular 0 0

Singularity at a point is singularity at the origin of the model translated there, parallel to equation_iff_variableChange and nonsingular_iff_variableChange.

theorem WeierstrassCurve.Affine.IsSingular.map {R : Type u_1} [CommRing R] {W : Affine R} {S : Type u_2} [CommRing S] (f : R →+* S) {x y : R} (h : W.IsSingular x y) : (W.map f).IsSingular (f x) (f y)

Singularity is carried along a coefficient map.

theorem WeierstrassCurve.Affine.map_isSingular {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} (hf : Function.Injective ⇑f) (W : Affine R) (x y : R) : (W.map f).IsSingular (f x) (f y) ↔ W.IsSingular x y

An injective coefficient map reflects singularity as well.

theorem WeierstrassCurve.Affine.IsSingular.baseChange {R : Type u_1} [CommRing R] {W : Affine R} {A : Type u_2} {B : Type u_3} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (f : A →ₐ[R] B) {x y : A} (h : (W.baseChange A).IsSingular x y) : (W.baseChange B).IsSingular (f x) (f y)

Singularity is carried along a base change.

theorem WeierstrassCurve.Affine.baseChange_isSingular {R : Type u_1} [CommRing R] {A : Type u_2} {B : Type u_3} [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] {f : A →ₐ[R] B} (hf : Function.Injective ⇑f) (W : Affine R) (x y : A) : (W.baseChange B).IsSingular (f x) (f y) ↔ (W.baseChange A).IsSingular x y

An injective base change reflects singularity as well.

theorem WeierstrassCurve.Affine.IsSingular.Δ_eq_zero {R : Type u_1} [CommRing R] {W : Affine R} {x y : R} (h : W.IsSingular x y) : Δ W = 0

A singular point forces the discriminant to vanish.

theorem WeierstrassCurve.Affine.exists_isSingular_of_Δ_eq_zero {F : Type u_2} [Field F] [PerfectField F] (W : Affine F) (hΔ : Δ W = 0) : ∃ (x : F) (y : F), W.IsSingular x y

A Weierstrass model of discriminant zero over a perfect field has a rational singular point. The perfectness hypothesis is used only for the inseparable residual cases in characteristics two and three; in particular, the theorem applies to every finite field.

theorem WeierstrassCurve.Affine.Δ_eq_zero_iff_exists_isSingular {F : Type u_2} [Field F] [PerfectField F] (W : Affine F) : Δ W = 0 ↔ ∃ (x : F) (y : F), W.IsSingular x y

Over a perfect field, a Weierstrass model is singular exactly when its discriminant vanishes.

theorem WeierstrassCurve.Affine.pow_sub_eq_zero_of_isSingular_of_isSingular {R : Type u_1} [CommRing R] {W : Affine R} {x₁ y₁ x₂ y₂ : R} (h₁ : W.IsSingular x₁ y₁) (h₂ : W.IsSingular x₂ y₂) : (x₂ - x₁) ^ 3 = 0 ∧ (y₂ - y₁) ^ 4 = 0

Two singular points of a Weierstrass model have (x₂ - x₁) ^ 3 = 0 and (y₂ - y₁) ^ 4 = 0. The nilpotence and equality forms below follow from these.

theorem WeierstrassCurve.Affine.isNilpotent_sub_of_isSingular_of_isSingular {R : Type u_1} [CommRing R] {W : Affine R} {x₁ y₁ x₂ y₂ : R} (h₁ : W.IsSingular x₁ y₁) (h₂ : W.IsSingular x₂ y₂) : IsNilpotent (x₂ - x₁) ∧ IsNilpotent (y₂ - y₁)

Each coordinate difference of two singular points of a Weierstrass model is nilpotent.

theorem WeierstrassCurve.Affine.eq_of_isSingular_of_isSingular {R : Type u_1} [CommRing R] {W : Affine R} {x₁ y₁ x₂ y₂ : R} [IsReduced R] (h₁ : W.IsSingular x₁ y₁) (h₂ : W.IsSingular x₂ y₂) : x₁ = x₂ ∧ y₁ = y₂

Over a reduced ring a Weierstrass model has at most one singular point.

theorem WeierstrassCurve.Affine.subsingleton_singular {R : Type u_1} [CommRing R] [IsReduced R] (W : Affine R) (p q : R × R) (hp : W.Equation p.1 p.2) (hp' : ¬W.Nonsingular p.1 p.2) (hq : W.Equation q.1 q.2) (hq' : ¬W.Nonsingular q.1 q.2) : p = q

A Weierstrass model over a reduced ring has at most one singular point, in Mathlib's vocabulary.