The Frey–Hellegouarch curve

For elements A and B of a commutative ring, the Frey–Hellegouarch curve is

y² = x (x - A) (x + B),

that is a₂ = B - A, a₄ = -A B and a₁ = a₃ = a₆ = 0. Its discriminant and c₄ are

Δ = 16 A² B² (A + B)², c₄ = 16 (A² + A B + B²),

so over a field of characteristic not 2 it is elliptic exactly when A, B and A + B are nonzero. Applied to a solution aᵖ + bᵖ + cᵖ = 0 of Fermat's equation with A = aᵖ and B = bᵖ, its three roots 0, A and -B differ by aᵖ, bᵖ and cᵖ; this is the curve of Frey's approach to Fermat's Last Theorem.

At 2 the equation above is not the one to reduce: 16 divides both c₄ and Δ. When A ≡ -1 (mod 4) and 16 ∣ B, the substitution x = 4 x', y = 8 y' + 4 x' divides c₄ by 2⁴ and Δ by 2¹², and gives the equation freyCurveModel α β, where A = 4 α - 1 and B = 16 β:

y² + x y = x³ + (4 β - α) x² - (4 α - 1) β x,

whose c₄ is A² + A B + B² and whose discriminant is (A β (A + B))² = A² B² (A + B)² / 2⁸. If moreover A and B are coprime, these two are coprime, so at every prime one of them is a unit: the model is globally minimal and every reduction is good or multiplicative. Over a Dedekind domain O with fraction field F, when the Frey curve is elliptic over F, it is therefore semistable, with minimal discriminant ideal (A² B² (A + B)² / 2⁸).

For Fermat's equation, the hypotheses on A and B can always be arranged. Exactly one of a, b, c is even, and permuting the triple puts it in the b position; the other two have p-th powers summing to 0 modulo 4, so one of them has p-th power ≡ -1 (mod 4), and swapping the odd entries if necessary puts it in the a position. Then A = aᵖ ≡ -1 (mod 4) and, for p ≥ 4, 16 ∣ B = bᵖ.

Main definitions

• TauCeti.freyCurve A B: the Weierstrass curve y² = x (x - A) (x + B) over a commutative ring.
• TauCeti.freyCurveModel α β: the equation y² + x y = x³ + (4 β - α) x² - (4 α - 1) β x, the integral model at 2 of freyCurve (4 α - 1) (16 β).

Main results

• TauCeti.freyCurve_Δ and TauCeti.freyCurve_c₄: Δ = 16 A² B² (A + B)² and c₄ = 16 (A² + A B + B²); TauCeti.freyCurve_Δ_eq_mul_sq writes Δ = 16 (A B (A + B))².
• TauCeti.isElliptic_freyCurve_iff and TauCeti.isElliptic_freyCurve_iff_ne_zero: the curve is elliptic exactly when 2, A, B and A + B are units, respectively, over a field of characteristic not 2, nonzero.
• TauCeti.isElliptic_baseChange_freyCurve: the Frey curve of integers A and B is elliptic over ℚ when A B (A + B) ≠ 0.
• TauCeti.freyCurve_j: its j-invariant is 256 (A² + A B + B²)³ / (A² B² (A + B)²).
• TauCeti.smul_freyCurve_eq_freyCurveModel: the change of variables x = 4 x', y = 8 y' + 4 x' carries freyCurve (4 α - 1) (16 β) to freyCurveModel α β.
• TauCeti.freyCurve_Δ_notMem_or_c₄_notMem: for coprime A and B, a prime not containing 2 does not contain both the discriminant and the c₄ of the Frey curve.
• TauCeti.isGlobalMinimal_baseChange_freyCurveModel: for coprime A and B, this model is globally minimal over a Dedekind domain, when it is elliptic over the fraction field.
• TauCeti.isSemistable_freyCurve and TauCeti.minimalDiscriminantIdeal_freyCurve: if A and B are coprime, A ≡ -1 (mod 4), 16 ∣ B and the Frey curve is elliptic over the fraction field, it is semistable with minimal discriminant ideal (A² B² (A + B)² / 2⁸).
• TauCeti.isGlobalMinimal_baseChange_freyCurve and TauCeti.minimalDiscriminantIdeal_freyCurve_of_not_dvd: over ℤ, if A and B are coprime and 16 ∤ A B (A + B), the equation y² = x (x - A) (x + B) itself is globally minimal, since 2¹² does not divide its discriminant (TauCeti.two_pow_twelve_dvd_freyCurve_Δ_iff), and its minimal discriminant is 16 (A B (A + B))².
• TauCeti.pow_modEq_neg_one_or_pow_modEq_neg_one: if xᵖ + eᵖ + yᵖ = 0 with e even, x coprime to e and p ≥ 2, then xᵖ or yᵖ is -1 modulo 4.
• TauCeti.exists_perm_two_dvd_and_pow_modEq_neg_one: a solution of aᵖ + bᵖ + cᵖ = 0 with a and b coprime and p ≥ 2 can be permuted so that b is even and aᵖ ≡ -1 (mod 4).
• TauCeti.isCoprime_of_gcd_eq_one_of_add_pow_eq_pow: if aⁿ + bⁿ = cⁿ and a, b, c have no common factor, then a and b are coprime.
• TauCeti.exists_isCoprime_and_mul_mul_add_eq_pow: a solution of aⁿ + bⁿ = cⁿ with a and b coprime and n ≥ 5, of either parity, gives coprime A ≡ -1 (mod 4) and B with 32 ∣ B and A B (A + B) = (a b c)ⁿ.
• TauCeti.isSemistable_freyCurve_pow and TauCeti.minimalDiscriminantIdeal_freyCurve_pow: for such a normalised solution with p ≥ 4, if the Frey curve of (aᵖ, bᵖ) is elliptic over ℚ, it is semistable over ℤ with minimal discriminant (a b c)^(2 p) / 2⁸.

References

• G. Frey, Links between stable elliptic curves and certain Diophantine equations, Ann. Univ. Sarav. Ser. Math. 1 (1986), 1–40.
• Y. Hellegouarch, Points d'ordre 2pʰ sur les courbes elliptiques, Acta Arith. 26 (1975), 253–263.
• H. Darmon, F. Diamond, R. Taylor, Fermat's Last Theorem, in Current Developments in Mathematics 1995, International Press (1995), 1–154.

def TauCeti.freyCurve {R : Type u_1} [CommRing R] (A B : R) : WeierstrassCurve R

The Frey–Hellegouarch curve y² = x (x - A) (x + B), that is a₂ = B - A and a₄ = -A B, the other coefficients being 0. Its roots 0, A and -B differ by A, B and A + B.

@[simp]

theorem TauCeti.freyCurve_a₁ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).a₁ = 0

@[simp]

theorem TauCeti.freyCurve_a₂ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).a₂ = B - A

@[simp]

theorem TauCeti.freyCurve_a₃ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).a₃ = 0

@[simp]

theorem TauCeti.freyCurve_a₄ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).a₄ = -(A * B)

@[simp]

theorem TauCeti.freyCurve_a₆ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).a₆ = 0

@[simp]

theorem TauCeti.freyCurve_b₂ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).b₂ = 4 * (B - A)

@[simp]

theorem TauCeti.freyCurve_b₄ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).b₄ = -2 * A * B

@[simp]

theorem TauCeti.freyCurve_b₆ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).b₆ = 0

@[simp]

theorem TauCeti.freyCurve_b₈ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).b₈ = -(A ^ 2 * B ^ 2)

@[simp]

theorem TauCeti.freyCurve_c₄ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).c₄ = 16 * (A ^ 2 + A * B + B ^ 2)

The c₄ of the Frey curve is 16 (A² + A B + B²).

@[simp]

theorem TauCeti.freyCurve_c₆ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).c₆ = -32 * (B - A) * (2 * A + B) * (A + 2 * B)

The c₆ of the Frey curve is -32 (B - A) (2 A + B) (A + 2 B).

@[simp]

theorem TauCeti.freyCurve_Δ {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).Δ = 16 * A ^ 2 * B ^ 2 * (A + B) ^ 2

The discriminant of the Frey curve is 16 A² B² (A + B)².

theorem TauCeti.freyCurve_Δ_eq_mul_sq {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).Δ = 16 * (A * B * (A + B)) ^ 2

The discriminant of the Frey curve is 16 (A B (A + B))².

@[simp]

theorem TauCeti.map_freyCurve {R : Type u_1} [CommRing R] (A B : R) {S : Type u_2} [CommRing S] (f : R →+* S) : (freyCurve A B).map f = freyCurve (f A) (f B)

The image of a Frey curve under a ring homomorphism is the Frey curve of the images.

theorem TauCeti.isElliptic_freyCurve_iff {R : Type u_1} [CommRing R] (A B : R) : (freyCurve A B).IsElliptic ↔ IsUnit 2 ∧ IsUnit A ∧ IsUnit B ∧ IsUnit (A + B)

The Frey curve is elliptic exactly when 2, A, B and A + B are units.

def TauCeti.freyCurveModel {R : Type u_1} [CommRing R] (α β : R) : WeierstrassCurve R

The Frey curve's equation at 2: y² + x y = x³ + (4 β - α) x² - (4 α - 1) β x. When A = 4 α - 1 and B = 16 β, it is obtained from freyCurve A B by x = 4 x', y = 8 y' + 4 x' (smul_freyCurve_eq_freyCurveModel), its c₄ is A² + A B + B² and its discriminant is (A β (A + B))² = A² B² (A + B)² / 2⁸.

@[simp]

theorem TauCeti.freyCurveModel_a₁ {R : Type u_1} [CommRing R] (α β : R) : (freyCurveModel α β).a₁ = 1

@[simp]

theorem TauCeti.freyCurveModel_a₂ {R : Type u_1} [CommRing R] (α β : R) : (freyCurveModel α β).a₂ = 4 * β - α

@[simp]

theorem TauCeti.freyCurveModel_a₃ {R : Type u_1} [CommRing R] (α β : R) : (freyCurveModel α β).a₃ = 0

@[simp]

theorem TauCeti.freyCurveModel_a₄ {R : Type u_1} [CommRing R] (α β : R) : (freyCurveModel α β).a₄ = -((4 * α - 1) * β)

@[simp]

theorem TauCeti.freyCurveModel_a₆ {R : Type u_1} [CommRing R] (α β : R) : (freyCurveModel α β).a₆ = 0

@[simp]

theorem TauCeti.freyCurveModel_c₄ {R : Type u_1} [CommRing R] (α β : R) : (freyCurveModel α β).c₄ = (4 * α - 1) ^ 2 + (4 * α - 1) * (16 * β) + (16 * β) ^ 2

The c₄ of freyCurveModel α β is A² + A B + B², where A = 4 α - 1 and B = 16 β; this is the c₄ of freyCurve A B divided by 2⁴.

@[simp]

theorem TauCeti.freyCurveModel_Δ {R : Type u_1} [CommRing R] (α β : R) : (freyCurveModel α β).Δ = ((4 * α - 1) * β * (4 * α - 1 + 16 * β)) ^ 2

The discriminant of freyCurveModel α β is (A β (A + B))², where A = 4 α - 1 and B = 16 β; this is the discriminant 16 A² B² (A + B)² of freyCurve A B divided by 2¹².

@[simp]

theorem TauCeti.map_freyCurveModel {R : Type u_1} [CommRing R] (α β : R) {S : Type u_2} [CommRing S] (f : R →+* S) : (freyCurveModel α β).map f = freyCurveModel (f α) (f β)

The image of the model under a ring homomorphism is the model of the images.

theorem TauCeti.isCoprime_freyCurveModel_Δ_c₄ {R : Type u_1} [CommRing R] {α β : R} (h : IsCoprime (4 * α - 1) (16 * β)) : IsCoprime (freyCurveModel α β).Δ (freyCurveModel α β).c₄

For coprime A = 4 α - 1 and B = 16 β, the discriminant and c₄ of freyCurveModel α β are coprime. The discriminant (A β (A + B))² divides a power of A B (A + B), which is coprime to c₄ = A² + A B + B² (IsCoprime.mul_mul_add_sq_add_mul_add_sq).

theorem TauCeti.freyCurve_Δ_notMem_or_c₄_notMem {R : Type u_1} [CommRing R] {A B : R} (hAB : IsCoprime A B) {P : Ideal R} [hP : P.IsPrime] (h2 : 2 ∉ P) : (freyCurve A B).Δ ∉ P ∨ (freyCurve A B).c₄ ∉ P

Away from 2, the Frey curve of a coprime pair has its discriminant or its c₄ outside a prime. Up to the factors 16, the discriminant 16 (A B (A + B))² and c₄ = 16 (A² + A B + B²) are coprime (IsCoprime.mul_mul_add_sq_add_mul_add_sq), so a prime not containing 2 does not contain both.

theorem TauCeti.isElliptic_freyCurve_iff_ne_zero {F : Type u_1} [Field F] (h2 : 2 ≠ 0) (A B : F) : (freyCurve A B).IsElliptic ↔ A ≠ 0 ∧ B ≠ 0 ∧ A + B ≠ 0

Over a field of characteristic not 2, the Frey curve is elliptic exactly when A, B and A + B are nonzero.

@[simp]

theorem TauCeti.freyCurve_j {F : Type u_1} [Field F] (A B : F) [(freyCurve A B).IsElliptic] : (freyCurve A B).j = 256 * (A ^ 2 + A * B + B ^ 2) ^ 3 / (A ^ 2 * B ^ 2 * (A + B) ^ 2)

The j-invariant of the Frey curve is 256 (A² + A B + B²)³ / (A² B² (A + B)²).

theorem TauCeti.smul_freyCurve_eq_freyCurveModel {F : Type u_1} [Field F] (h2 : 2 ≠ 0) (α β : F) : { u := Units.mk0 2 h2, r := 0, s := 1, t := 0 } • freyCurve (4 * α - 1) (16 * β) = freyCurveModel α β

The change of variables x = 4 x', y = 8 y' + 4 x' carries freyCurve (4 α - 1) (16 β) to freyCurveModel α β.

theorem TauCeti.isGlobalMinimal_baseChange_freyCurveModel {O : Type u_1} [CommRing O] [IsDedekindDomain O] {F : Type u_2} [Field F] [Algebra O F] [IsFractionRing O F] {α β : O} [((freyCurveModel α β).baseChange F).IsElliptic] (h : IsCoprime (4 * α - 1) (16 * β)) : WeierstrassCurve.IsGlobalMinimal O ((freyCurveModel α β).baseChange F)

For coprime 4 α - 1 and 16 β, the model freyCurveModel α β is globally minimal, when it is elliptic over the fraction field F.

theorem TauCeti.isSemistable_freyCurve {O : Type u_1} [CommRing O] [IsDedekindDomain O] {F : Type u_2} [Field F] [Algebra O F] [IsFractionRing O F] {A B : O} (hA : 4 ∣ A + 1) (hB : 16 ∣ B) (hAB : IsCoprime A B) [((freyCurve A B).baseChange F).IsElliptic] : WeierstrassCurve.IsSemistable O ((freyCurve A B).baseChange F)

The Frey curve is semistable over a Dedekind domain O when it is elliptic over the fraction field F, A and B are coprime, A ≡ -1 (mod 4) and 16 ∣ B: its model at 2 has coprime discriminant and c₄, so the reduction at every height-one prime is good or multiplicative.

theorem TauCeti.minimalDiscriminantIdeal_freyCurve {O : Type u_1} [CommRing O] [IsDedekindDomain O] {F : Type u_2} [Field F] [Algebra O F] [IsFractionRing O F] {A B d : O} (hA : 4 ∣ A + 1) (hB : 16 ∣ B) (hAB : IsCoprime A B) (hd : 2 ^ 8 * d = A ^ 2 * B ^ 2 * (A + B) ^ 2) [((freyCurve A B).baseChange F).IsElliptic] : WeierstrassCurve.minimalDiscriminantIdeal O ((freyCurve A B).baseChange F) = Ideal.span {d}

The minimal discriminant ideal of the Frey curve is (A² B² (A + B)² / 2⁸) when it is elliptic over the fraction field F, A and B are coprime, A ≡ -1 (mod 4) and 16 ∣ B. The quotient by 2⁸ is the element d with 2⁸ d = A² B² (A + B)²; it is the discriminant of the globally minimal model at 2.

theorem TauCeti.isElliptic_baseChange_freyCurve {A B : ℤ} (h : A * B * (A + B) ≠ 0) : ((freyCurve A B).baseChange ℚ).IsElliptic

The Frey curve of integers A and B with A B (A + B) ≠ 0 is elliptic over ℚ.

theorem TauCeti.two_pow_twelve_dvd_freyCurve_Δ_iff {A B : ℤ} : 2 ^ 12 ∣ (freyCurve A B).Δ ↔ 16 ∣ A * B * (A + B)

2¹² divides the discriminant 16 (A B (A + B))² of the Frey curve over ℤ exactly when 16 divides A B (A + B), since 2¹² = 16 · 16².

theorem TauCeti.isGlobalMinimal_baseChange_freyCurve {A B : ℤ} (hAB : IsCoprime A B) (h16 : ¬16 ∣ A * B * (A + B)) [((freyCurve A B).baseChange ℚ).IsElliptic] : WeierstrassCurve.IsGlobalMinimal ℤ ((freyCurve A B).baseChange ℚ)

The Frey equation is globally minimal over ℤ when 16 ∤ A B (A + B), for coprime A and B. At 2 its discriminant 16 (A B (A + B))² has valuation less than 12 (TauCeti.two_pow_twelve_dvd_freyCurve_Δ_iff); away from 2 its discriminant or its c₄ is a unit (TauCeti.freyCurve_Δ_notMem_or_c₄_notMem).

theorem TauCeti.minimalDiscriminantIdeal_freyCurve_of_not_dvd {A B : ℤ} (hAB : IsCoprime A B) (h16 : ¬16 ∣ A * B * (A + B)) [((freyCurve A B).baseChange ℚ).IsElliptic] : WeierstrassCurve.minimalDiscriminantIdeal ℤ ((freyCurve A B).baseChange ℚ) = Ideal.span {16 * (A * B * (A + B)) ^ 2}

The minimal discriminant of the Frey curve is 16 (A B (A + B))² when 16 ∤ A B (A + B), for coprime A and B: the Frey equation is then globally minimal.

theorem TauCeti.pow_modEq_neg_one_or_pow_modEq_neg_one {p : ℕ} (hp : 2 ≤ p) {x e y : ℤ} (he : 2 ∣ e) (hx : IsCoprime x e) (h : x ^ p + e ^ p + y ^ p = 0) : x ^ p ≡ -1 [ZMOD 4] ∨ y ^ p ≡ -1 [ZMOD 4]

If x is coprime to an even e, and xᵖ + eᵖ + yᵖ = 0 with p ≥ 2, then xᵖ or yᵖ is -1 modulo 4: both are odd and xᵖ + yᵖ ≡ 0 (mod 4).

theorem TauCeti.exists_perm_two_dvd_and_pow_modEq_neg_one {p : ℕ} (hp : 2 ≤ p) {a b c : ℤ} (hab : IsCoprime a b) (h : a ^ p + b ^ p + c ^ p = 0) : ∃ (a' : ℤ) (b' : ℤ) (c' : ℤ), [a', b', c'].Perm [a, b, c] ∧ 2 ∣ b' ∧ a' ^ p ≡ -1 [ZMOD 4]

The normalisation of a Fermat triple. If aᵖ + bᵖ + cᵖ = 0 with a and b coprime and p ≥ 2, some permutation a', b', c' of a, b, c has b' even and a'ᵖ ≡ -1 (mod 4). The three entries are then pairwise coprime, so exactly one of them is even, and it is put in the middle; the other two have p-th powers summing to 0 modulo 4, and one of them is chosen first. No entry needs to be negated.

theorem TauCeti.isCoprime_of_gcd_eq_one_of_add_pow_eq_pow {n : ℕ} {a b c : ℤ} (hgcd : {a, b, c}.gcd id = 1) (h : a ^ n + b ^ n = c ^ n) : IsCoprime a b

If aⁿ + bⁿ = cⁿ and a, b, c have no common factor, then a and b are coprime: a prime dividing both divides cⁿ, hence c. This is the analogue of Mathlib's isCoprime_of_gcd_eq_one_of_FLT for the form aⁿ + bⁿ = cⁿ, which covers even exponents.

theorem TauCeti.exists_isCoprime_and_mul_mul_add_eq_pow {n : ℕ} (hn : 5 ≤ n) {a b c : ℤ} (hab : IsCoprime a b) (h : a ^ n + b ^ n = c ^ n) : ∃ (A : ℤ) (B : ℤ), IsCoprime A B ∧ 4 ∣ A + 1 ∧ 32 ∣ B ∧ A * B * (A + B) = (a * b * c) ^ n

The Frey curve of a Fermat triple. If aⁿ + bⁿ = cⁿ with a and b coprime and n ≥ 5, there are coprime integers A and B with A ≡ -1 (mod 4), 32 ∣ B and A B (A + B) = (a b c)ⁿ. Here B is the even one of aⁿ, bⁿ, cⁿ, up to sign, and A is one of the other two, up to sign.

theorem TauCeti.isSemistable_freyCurve_pow {p : ℕ} (hp : 4 ≤ p) {a b : ℤ} (hab : IsCoprime a b) (hb : 2 ∣ b) (ha : a ^ p ≡ -1 [ZMOD 4]) [((freyCurve (a ^ p) (b ^ p)).baseChange ℚ).IsElliptic] : WeierstrassCurve.IsSemistable ℤ ((freyCurve (a ^ p) (b ^ p)).baseChange ℚ)

The Frey curve of a normalised Fermat triple is semistable. If a and b are coprime, b is even, aᵖ ≡ -1 (mod 4), p ≥ 4 and y² = x (x - aᵖ) (x + bᵖ) is elliptic over ℚ, then it is semistable over ℤ.

theorem TauCeti.minimalDiscriminantIdeal_freyCurve_pow {p : ℕ} (hp : 4 ≤ p) {a b c : ℤ} (hab : IsCoprime a b) (h : a ^ p + b ^ p + c ^ p = 0) (hb : 2 ∣ b) (ha : a ^ p ≡ -1 [ZMOD 4]) [((freyCurve (a ^ p) (b ^ p)).baseChange ℚ).IsElliptic] : WeierstrassCurve.minimalDiscriminantIdeal ℤ ((freyCurve (a ^ p) (b ^ p)).baseChange ℚ) = Ideal.span {(a * b * c) ^ (2 * p) / 2 ^ 8}

The minimal discriminant of the Frey curve of a Fermat triple is (a b c)^(2 p) / 2⁸. If aᵖ + bᵖ + cᵖ = 0 with a and b coprime, b even, aᵖ ≡ -1 (mod 4) and p ≥ 4, and y² = x (x - aᵖ) (x + bᵖ) is elliptic over ℚ, its minimal discriminant ideal over ℤ is generated by (a b c)^(2 p) / 2⁸.