Normal forms: transport, changes of variables, and elementary consequences #

Mathlib's WeierstrassCurve.IsCharNeTwoNF asserts a₁ = a₃ = 0 and its WeierstrassCurve.IsShortNF asserts a₁ = a₂ = a₃ = 0, and its NormalForms file proves a great deal from those hypotheses. This file collects four things it does not record.

Transport. Both conditions are preserved by map and baseChange — the coefficients of W.map f are the images of W's, so a vanishing coefficient stays vanishing.

Completing the square. The change toCharNeTwoNF gives explicit formulas for its three remaining coefficients.

Changes of variables between short normal forms. When 2 and 3 are non-zero-divisors, a change of variables carrying one short equation to another is a pure scaling (x, y) ↦ (u²x, u³y): its r, s and t vanish, so it acts on the coefficients by (a₄, a₆) ↦ (u⁻⁴a₄, u⁻⁶a₆). This is the only freedom left in a short equation, and it is what a canonical short equation has to normalise away.

Elementary consequences. Facts that follow from a₁ = a₃ = 0 alone, by unfolding negY, with no further machinery. y_eq_zero_of_order_two is the current example: negation is (x, y) ↦ (x, -y), so a 2-torsion point has y = 0. It lives here rather than with the division-polynomial material that first proved it because it needs none of that — this module's closure is one file, against thirty-three for DivisionPolynomial/ShortNagellLutz.lean — and its consumers, Nagell–Lutz and the 2-descent torsion count, sit in unrelated parts of the library.

That gap matters as soon as a statement is about a curve over ℤ and a point over ℚ, which is the shape of the classical Nagell–Lutz theorem: the hypothesis is natural on the integral model, while the point lives on the base change, and without these instances the class has to be re-established by hand at every such crossing.

Main results #

WeierstrassCurve.isCharNeTwoNF_map: a₁ = a₃ = 0 is preserved by a ring hom.
WeierstrassCurve.isCharNeTwoNF_baseChange: the same for a base change, which is the spelling consumers hold. Both are instances, so the crossing is silent.
WeierstrassCurve.isShortNF_map and WeierstrassCurve.isShortNF_baseChange: the same two statements for short normal form.
WeierstrassCurve.VariableChange.r_eq_zero_of_isShortNF, …s_eq_zero_of_isShortNF and …t_eq_zero_of_isShortNF: a change of variables between short normal forms is a scaling.
WeierstrassCurve.variableChange_a₄_of_isShortNF and WeierstrassCurve.variableChange_a₆_of_isShortNF: it acts on the coefficients by (a₄, a₆) ↦ (u⁻⁴a₄, u⁻⁶a₆).
WeierstrassCurve.y_eq_zero_of_order_two: in a characteristic-≠-2 normal form, an affine point killed by 2 has y = 0.
TauCeti.toCharNeTwoNF_a₂, TauCeti.toCharNeTwoNF_a₄, and TauCeti.toCharNeTwoNF_a₆: the coefficients after completing the square.

source

instance WeierstrassCurve.isCharNeTwoNF_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) [W.IsCharNeTwoNF] :

(W.map f).IsCharNeTwoNF

Characteristic-≠-2 normal form is preserved by a ring hom. (W.map f).a₁ is f W.a₁, and a hom sends 0 to 0, so the vanishing survives.

As an instance, this is what lets typeclass search carry IsCharNeTwoNF across W.map f: a caller who has the hypothesis on W and a statement about W.map f needs no bridging term.

source

instance WeierstrassCurve.isCharNeTwoNF_baseChange {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] [W.IsCharNeTwoNF] :

(W.baseChange S).IsCharNeTwoNF

Characteristic-≠-2 normal form is preserved by a base change. This is isCharNeTwoNF_map at algebraMap R S, stated separately because baseChange is the spelling a caller holds and instance search does not unfold it.

source

instance WeierstrassCurve.isShortNF_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) [W.IsShortNF] :

(W.map f).IsShortNF

Short normal form is preserved by a ring hom. (W.map f).a₂ is f W.a₂, and a hom sends 0 to 0, so the vanishing survives; likewise for a₁ and a₃. As an instance, it carries IsShortNF across W.map f in typeclass search.

source

instance WeierstrassCurve.isShortNF_baseChange {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] [W.IsShortNF] :

(W.baseChange S).IsShortNF

Short normal form is preserved by a base change. This is isShortNF_map at algebraMap R S, stated separately because baseChange is the spelling a caller holds and instance search does not unfold it.

Changes of variables between short normal forms #

The coefficients a₁, a₃ and a₂ of C • W are u⁻¹ · 2s, u⁻³ · 2t and u⁻² · 3r when W is short, so if C • W is short as well and 2 and 3 are non-zero-divisors then r = s = t = 0, and C is the scaling (x, y) ↦ (u²x, u³y).

source

theorem WeierstrassCurve.VariableChange.s_eq_zero_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) [W.IsShortNF] [(C • W).IsShortNF] (h2 : IsRegular 2) :

C.s = 0

A change of variables between short normal forms has s = 0, when 2 is a non-zero-divisor.

source

theorem WeierstrassCurve.VariableChange.t_eq_zero_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) [W.IsShortNF] [(C • W).IsShortNF] (h2 : IsRegular 2) :

C.t = 0

A change of variables between short normal forms has t = 0, when 2 is a non-zero-divisor.

source

theorem WeierstrassCurve.VariableChange.r_eq_zero_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) [W.IsShortNF] [(C • W).IsShortNF] (h2 : IsRegular 2) (h3 : IsRegular 3) :

C.r = 0

A change of variables between short normal forms has r = 0, when 2 and 3 are non-zero-divisors.

source

@[simp]

theorem WeierstrassCurve.variableChange_a₄_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) [W.IsShortNF] [(C • W).IsShortNF] (h2 : IsRegular 2) (h3 : IsRegular 3) :

(C • W).a₄ = ↑C.u⁻¹ ^ 4 * W.a₄

Between short normal forms, a change of variables scales a₄ by u⁻⁴, when 2 and 3 are non-zero-divisors.

source

@[simp]

theorem WeierstrassCurve.variableChange_a₆_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (C : VariableChange R) [W.IsShortNF] [(C • W).IsShortNF] (h2 : IsRegular 2) (h3 : IsRegular 3) :

(C • W).a₆ = ↑C.u⁻¹ ^ 6 * W.a₆

Between short normal forms, a change of variables scales a₆ by u⁻⁶, when 2 and 3 are non-zero-divisors.

source

theorem WeierstrassCurve.y_eq_zero_of_order_two {F : Type u_3} [Field F] [DecidableEq F] {E : WeierstrassCurve F} [E.IsCharNeTwoNF] (h2F : 2 ≠ 0) {x y : F} (hns : E.toAffine.Nonsingular x y) (h2 : 2 • Affine.Point.some x y hns = 0) :

y = 0

In characteristic-≠-2 normal form, a two-torsion point has y = 0. Negation is (x, y) ↦ (x, -y), so a point equal to its own negative has 2y = 0; cancelling 2 finishes it.

Nothing here sees ℤ or ℚ, and nothing needs a₂ = 0: the argument is the normal-form identity plus the ability to cancel 2 in the point's own field, so those are exactly the hypotheses.

The hypothesis is annihilation by 2 rather than addOrderOf P = 2, which is what the proof and every caller actually have. For an affine point the two are equivalent — Point.some _ _ _ is never 0 — so the name remains exact; the weaker form simply spares callers the reconstruction.

source

@[simp]