The reduced minimal equation of an elliptic curve over ℚ

Every elliptic curve E over ℚ has a Weierstrass equation that is minimal at every prime (WeierstrassCurve.exists_isGlobalMinimal_smul, ℤ being a principal ideal domain). Such an equation is not unique: the changes of variables between globally minimal equations are exactly those defined over ℤ (WeierstrassCurve.IsGlobalMinimal.exists_baseChange_eq_of_smul_eq), with u = ±1 and r, s, t ∈ ℤ. Using that freedom to reduce a₁ modulo 2, then a₂ modulo 3, then a₃ modulo 2 gives the reduced minimal equation, with

a₁ ∈ {0, 1}, a₂ ∈ {-1, 0, 1}, a₃ ∈ {0, 1}.

It is unique: a change of variables over ℤ between two reduced equations is the identity or the negation automorphism [-1], both of which fix the equation. This is the equation by which tables of elliptic curves over ℚ (Cremona's tables, the LMFDB) present a curve, so it lets a label name an equation rather than an isomorphism class.

The reduced minimal equation is a long Weierstrass equation. It is a different object from the minimal-pair short equation WeierstrassCurve.minimalPairModel, which need not be minimal at 2 and 3.

Main definitions

• WeierstrassCurve.IsReducedMinimal W: W is globally minimal over ℤ with a₁, a₃ ∈ {0, 1} and a₂ ∈ {-1, 0, 1}.
• WeierstrassCurve.reducedMinimalModel E: the reduced minimal equation of E.

Main results

• WeierstrassCurve.exists_isReducedMinimal_smul: every elliptic curve over ℚ has a reduced minimal equation.
• WeierstrassCurve.IsReducedMinimal.eq_of_smul_eq: two reduced minimal equations related by a change of variables are equal.
• WeierstrassCurve.existsUnique_reducedMinimal: the reduced minimal equation in the variable-change orbit of E exists and is unique. The change of variables reaching it is not unique: it may be composed with [-1].
• WeierstrassCurve.eq_reducedMinimalModel and WeierstrassCurve.VariableChange.reducedMinimalModel_smul: the reduced minimal model is characterised by being reduced minimal and isomorphic to E, so it is invariant under a change of variables.
• WeierstrassCurve.IsReducedMinimal.reducedMinimalModel_eq and WeierstrassCurve.reducedMinimalModel_reducedMinimalModel: reduced equations are fixed by the construction, so it is idempotent.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.1 and VIII.8.
• J. E. Cremona, Algorithms for Modular Elliptic Curves, 2nd ed., Cambridge University Press, 1997: the normalisation a₁, a₃ ∈ {0, 1}, a₂ ∈ {-1, 0, 1} of a minimal equation.

def WeierstrassCurve.IsReducedMinimal (W : WeierstrassCurve ℚ) [W.IsElliptic] : Prop

A reduced minimal Weierstrass equation over ℚ: globally minimal over ℤ, with the residual freedom of the changes of variables over ℤ pinned by a₁, a₃ ∈ {0, 1} and a₂ ∈ {-1, 0, 1}. Every elliptic curve over ℚ has exactly one such equation in its variable-change orbit (existsUnique_reducedMinimal).

Equations

• W.IsReducedMinimal = (WeierstrassCurve.IsGlobalMinimal ℤ W ∧ (W.a₁ = 0 ∨ W.a₁ = 1) ∧ (W.a₂ = -1 ∨ W.a₂ = 0 ∨ W.a₂ = 1) ∧ (W.a₃ = 0 ∨ W.a₃ = 1))

@[simp]

theorem WeierstrassCurve.isReducedMinimal_iff {W : WeierstrassCurve ℚ} [W.IsElliptic] : W.IsReducedMinimal ↔ IsGlobalMinimal ℤ W ∧ (W.a₁ = 0 ∨ W.a₁ = 1) ∧ (W.a₂ = -1 ∨ W.a₂ = 0 ∨ W.a₂ = 1) ∧ (W.a₃ = 0 ∨ W.a₃ = 1)

Reduced minimality, unfolded. This is the interface to WeierstrassCurve.IsReducedMinimal outside its defining module.

theorem WeierstrassCurve.IsReducedMinimal.isGlobalMinimal {W : WeierstrassCurve ℚ} [W.IsElliptic] (h : W.IsReducedMinimal) : IsGlobalMinimal ℤ W

A reduced minimal equation is globally minimal over ℤ.

The normalisation over ℤ

theorem WeierstrassCurve.exists_variableChange_reduced (W : WeierstrassCurve ℤ) : ∃ (C : VariableChange ℤ), ((C • W).a₁ = 0 ∨ (C • W).a₁ = 1) ∧ ((C • W).a₂ = -1 ∨ (C • W).a₂ = 0 ∨ (C • W).a₂ = 1) ∧ ((C • W).a₃ = 0 ∨ (C • W).a₃ = 1)

Every equation over ℤ is carried to one with a₁, a₃ ∈ {0, 1} and a₂ ∈ {-1, 0, 1} by a change of variables over ℤ.

theorem WeierstrassCurve.VariableChange.smul_eq_self_of_reduced {W : WeierstrassCurve ℤ} (C : VariableChange ℤ) (h₁ : W.a₁ = 0 ∨ W.a₁ = 1) (h₂ : W.a₂ = -1 ∨ W.a₂ = 0 ∨ W.a₂ = 1) (h₃ : W.a₃ = 0 ∨ W.a₃ = 1) (h₁' : (C • W).a₁ = 0 ∨ (C • W).a₁ = 1) (h₂' : (C • W).a₂ = -1 ∨ (C • W).a₂ = 0 ∨ (C • W).a₂ = 1) (h₃' : (C • W).a₃ = 0 ∨ (C • W).a₃ = 1) : C • W = W

A change of variables over ℤ between two equations in reduced form fixes the equation: it is the identity when u = 1, and the negation automorphism when u = -1.

Existence and uniqueness

theorem WeierstrassCurve.exists_isReducedMinimal_smul (E : WeierstrassCurve ℚ) [E.IsElliptic] : ∃ (C : VariableChange ℚ), (C • E).IsReducedMinimal

Every elliptic curve over ℚ has a reduced minimal equation in its variable-change orbit.

theorem WeierstrassCurve.IsReducedMinimal.eq_of_smul_eq {W₁ W₂ : WeierstrassCurve ℚ} [W₁.IsElliptic] [W₂.IsElliptic] (h₁ : W₁.IsReducedMinimal) (h₂ : W₂.IsReducedMinimal) (C : VariableChange ℚ) (hC : C • W₁ = W₂) : W₁ = W₂

Two reduced minimal equations related by a change of variables are equal. This gives uniqueness of the reduced equation in each variable-change orbit.

theorem WeierstrassCurve.existsUnique_reducedMinimal (E : WeierstrassCurve ℚ) [E.IsElliptic] : ∃! W : { W : WeierstrassCurve ℚ // W.IsElliptic }, (↑W).IsReducedMinimal ∧ ∃ (C : VariableChange ℚ), C • E = ↑W

Existence and uniqueness of the reduced minimal equation: the variable-change orbit of an elliptic curve over ℚ contains exactly one reduced minimal equation. The equation is unique; the change of variables reaching it is not, since it may be composed with [-1].

The reduced minimal model of a curve

noncomputable def WeierstrassCurve.reducedMinimalModel (E : WeierstrassCurve ℚ) [E.IsElliptic] : WeierstrassCurve ℚ

The reduced minimal model of an elliptic curve over ℚ: the unique reduced minimal equation in its variable-change orbit. It is characterised by isReducedMinimal_reducedMinimalModel, exists_smul_eq_reducedMinimalModel and eq_reducedMinimalModel, fixes reduced equations, and depends only on the ℚ-isomorphism class of E (VariableChange.reducedMinimalModel_smul).

Equations

• E.reducedMinimalModel = ⋯.choose • E

theorem WeierstrassCurve.exists_smul_eq_reducedMinimalModel (E : WeierstrassCurve ℚ) [E.IsElliptic] : ∃ (C : VariableChange ℚ), C • E = E.reducedMinimalModel

The reduced minimal model is obtained from E by a change of variables.

instance WeierstrassCurve.isElliptic_reducedMinimalModel (E : WeierstrassCurve ℚ) [E.IsElliptic] : E.reducedMinimalModel.IsElliptic

The reduced minimal model of an elliptic curve is an elliptic curve.

theorem WeierstrassCurve.isReducedMinimal_reducedMinimalModel (E : WeierstrassCurve ℚ) [E.IsElliptic] : E.reducedMinimalModel.IsReducedMinimal

The reduced minimal model is reduced minimal.

theorem WeierstrassCurve.eq_reducedMinimalModel {E W : WeierstrassCurve ℚ} [E.IsElliptic] [W.IsElliptic] (hW : W.IsReducedMinimal) (C : VariableChange ℚ) (hC : C • E = W) : W = E.reducedMinimalModel

A reduced minimal equation isomorphic to E is the reduced minimal model of E.

theorem WeierstrassCurve.IsReducedMinimal.reducedMinimalModel_eq {W : WeierstrassCurve ℚ} [W.IsElliptic] (hW : W.IsReducedMinimal) : W.reducedMinimalModel = W

A reduced minimal equation is its own reduced minimal model.

@[simp]

theorem WeierstrassCurve.reducedMinimalModel_reducedMinimalModel (E : WeierstrassCurve ℚ) [E.IsElliptic] : E.reducedMinimalModel.reducedMinimalModel = E.reducedMinimalModel

Taking the reduced minimal model twice has the same result as taking it once.

@[simp]

theorem WeierstrassCurve.VariableChange.reducedMinimalModel_smul (C : VariableChange ℚ) (E : WeierstrassCurve ℚ) [E.IsElliptic] : (C • E).reducedMinimalModel = E.reducedMinimalModel

The reduced minimal model is an isomorphism invariant: it is unchanged by a change of variables.