Fermat Last Theorem in the case n = 3

The goal of this file is to prove Fermat Last theorem in the case n = 3.

Main results

• fermatLastTheoremThree_case1: the first case of Fermat Last Theorem when n = 3: if a b c : ℤ are such that ¬ 3 ∣ a * b * c, then a ^ 3 + b ^ 3 ≠ c ^ 3.

TODO

Prove case 2.

theorem fermatLastTheoremThree_case_1 {a : ℤ} {b : ℤ} {c : ℤ} (hdvd : ¬3 ∣ a * b * c) : a ^ 3 + b ^ 3 ≠ c ^ 3

If a b c : ℤ are such that ¬ 3 ∣ a * b * c, then a ^ 3 + b ^ 3 ≠ c ^ 3.

theorem fermatLastTheoremThree_of_three_dvd_only_c (H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) : FermatLastTheoremFor 3

To prove Fermat's Last Theorem for n = 3, it is enough to show that that for all a, b, c in ℤ such that c ≠ 0, ¬ 3 ∣ a, ¬ 3 ∣ b, a and b are coprime and 3 ∣ c, we have a ^ 3 + b ^ 3 ≠ c ^ 3.

def FermatLastTheoremForThreeGen {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑3) : Prop

FermatLastTheoremForThreeGen is the statement that a ^ 3 + b ^ 3 = u * c ^ 3 has no nontrivial solutions in 𝓞 K for all u : (𝓞 K)ˣ such that ¬ λ ∣ a, ¬ λ ∣ b and λ ∣ c. The reason to consider FermatLastTheoremForThreeGen is to make a descent argument working.

Equations

• One or more equations did not get rendered due to their size.

theorem FermatLastTheoremForThree_of_FermatLastTheoremThreeGen {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑3) : FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3

To prove FermatLastTheoremFor 3, it is enough to prove FermatLastTheoremForThreeGen.

structure FermatLastTheoremForThreeGen.Solution' {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑3) : Type u_1

Solution' is a tuple given by a solution to a ^ 3 + b ^ 3 = u * c ^ 3, where a, b, c and u are as in FermatLastTheoremForThreeGen. See Solution for the actual structure on which we will do the descent.

• a : NumberField.RingOfIntegers K
• b : NumberField.RingOfIntegers K
• c : NumberField.RingOfIntegers K
• u : (NumberField.RingOfIntegers K)ˣ
• ha : ¬hζ.toInteger - 1 ∣ self.a
• hb : ¬hζ.toInteger - 1 ∣ self.b
• hc : self.c ≠ 0
• coprime : IsCoprime self.a self.b
• hcdvd : hζ.toInteger - 1 ∣ self.c
• H : self.a ^ 3 + self.b ^ 3 = ↑self.u * self.c ^ 3

theorem FermatLastTheoremForThreeGen.Solution'.ha {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (self : FermatLastTheoremForThreeGen.Solution' hζ) : ¬hζ.toInteger - 1 ∣ self.a

theorem FermatLastTheoremForThreeGen.Solution'.hb {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (self : FermatLastTheoremForThreeGen.Solution' hζ) : ¬hζ.toInteger - 1 ∣ self.b

theorem FermatLastTheoremForThreeGen.Solution'.hc {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (self : FermatLastTheoremForThreeGen.Solution' hζ) : self.c ≠ 0

theorem FermatLastTheoremForThreeGen.Solution'.coprime {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (self : FermatLastTheoremForThreeGen.Solution' hζ) : IsCoprime self.a self.b

theorem FermatLastTheoremForThreeGen.Solution'.hcdvd {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (self : FermatLastTheoremForThreeGen.Solution' hζ) : hζ.toInteger - 1 ∣ self.c

theorem FermatLastTheoremForThreeGen.Solution'.H {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (self : FermatLastTheoremForThreeGen.Solution' hζ) : self.a ^ 3 + self.b ^ 3 = ↑self.u * self.c ^ 3

structure FermatLastTheoremForThreeGen.Solution {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑3) extends FermatLastTheoremForThreeGen.Solution' : Type u_1

Solution is the same as Solution' with the additional assumption that λ ^ 2 ∣ a + b.

• a : NumberField.RingOfIntegers K
• b : NumberField.RingOfIntegers K
• c : NumberField.RingOfIntegers K
• u : (NumberField.RingOfIntegers K)ˣ
• ha : ¬hζ.toInteger - 1 ∣ self.a
• hb : ¬hζ.toInteger - 1 ∣ self.b
• hc : self.c ≠ 0
• coprime : IsCoprime self.a self.b
• hcdvd : hζ.toInteger - 1 ∣ self.c
• H : self.a ^ 3 + self.b ^ 3 = ↑self.u * self.c ^ 3
• hab : (hζ.toInteger - 1) ^ 2 ∣ self.a + self.b

theorem FermatLastTheoremForThreeGen.Solution.hab {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (self : FermatLastTheoremForThreeGen.Solution hζ) : (hζ.toInteger - 1) ^ 2 ∣ self.a + self.b

theorem FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) : multiplicity.Finite (hζ.toInteger - 1) S'.c

For any S' : Solution', the multiplicity of λ in S'.c is finite.

def FermatLastTheoremForThreeGen.Solution'.multiplicity {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : ℕ

Given S' : Solution', S'.multiplicity is the multiplicity of λ in S'.c, as a natural number.

Equations

• S'.multiplicity = (multiplicity (hζ.toInteger - 1) S'.c).get ⋯

def FermatLastTheoremForThreeGen.Solution.multiplicity {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S : FermatLastTheoremForThreeGen.Solution hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : ℕ

Given S : Solution, S.multiplicity is the multiplicity of λ in S.c, as a natural number.

Equations

• S.multiplicity = S.multiplicity

def FermatLastTheoremForThreeGen.Solution.isMinimal {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S : FermatLastTheoremForThreeGen.Solution hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : Prop

We say that S : Solution is minimal if for all S₁ : Solution, the multiplicity of λ in S.c is less or equal than the multiplicity in S₁.c.

Equations

• S.isMinimal = ∀ (S₁ : FermatLastTheoremForThreeGen.Solution hζ), S.multiplicity ≤ S₁.multiplicity

theorem FermatLastTheoremForThreeGen.Solution.exists_minimal {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S : FermatLastTheoremForThreeGen.Solution hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : ∃ (S₁ : FermatLastTheoremForThreeGen.Solution hζ), S₁.isMinimal

If there is a solution then there is a minimal one.

theorem FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) : (hζ.toInteger - 1) ^ 4 ∣ S'.a ^ 3 - 1 ∧ (hζ.toInteger - 1) ^ 4 ∣ S'.b ^ 3 + 1 ∨ (hζ.toInteger - 1) ^ 4 ∣ S'.a ^ 3 + 1 ∧ (hζ.toInteger - 1) ^ 4 ∣ S'.b ^ 3 - 1

Given S' : Solution', then S'.a and S'.b are both congruent to 1 modulo λ ^ 4 or are both congruent to -1.

theorem FermatLastTheoremForThreeGen.lambda_pow_four_dvd_c_cube {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) : (hζ.toInteger - 1) ^ 4 ∣ S'.c ^ 3

Given S' : Solution', we have that λ ^ 4 divides S'.c ^ 3.

theorem FermatLastTheoremForThreeGen.lambda_sq_dvd_c {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : (hζ.toInteger - 1) ^ 2 ∣ S'.c

Given S' : Solution', we have that λ ^ 2 divides S'.c.

theorem FermatLastTheoremForThreeGen.Solution'.two_le_multiplicity {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : 2 ≤ S'.multiplicity

Given S' : Solution', we have that 2 ≤ S'.multiplicity.

theorem FermatLastTheoremForThreeGen.Solution.two_le_multiplicity {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S : FermatLastTheoremForThreeGen.Solution hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : 2 ≤ S.multiplicity

Given S : Solution, we have that 2 ≤ S.multiplicity.

theorem FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) : S'.a ^ 3 + S'.b ^ 3 = (S'.a + S'.b) * (S'.a + ↑⋯.unit * S'.b) * (S'.a + ↑⋯.unit ^ 2 * S'.b)

Given S' : Solution', the key factorization of S'.a ^ 3 + S'.b ^ 3.

theorem FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : (hζ.toInteger - 1) ^ 2 ∣ S'.a + S'.b ∨ (hζ.toInteger - 1) ^ 2 ∣ S'.a + ↑⋯.unit * S'.b ∨ (hζ.toInteger - 1) ^ 2 ∣ S'.a + ↑⋯.unit ^ 2 * S'.b

Given S' : Solution', we have that λ ^ 2 divides one amongst S'.a + S'.b, S'.a + η * S'.b and S'.a + η ^ 2 * S'.b.

theorem FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : ∃ (a' : NumberField.RingOfIntegers K) (b' : NumberField.RingOfIntegers K), a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬hζ.toInteger - 1 ∣ a' ∧ ¬hζ.toInteger - 1 ∣ b' ∧ (hζ.toInteger - 1) ^ 2 ∣ a' + b'

Given S' : Solution', we may assume that λ ^ 2 divides S'.a + S'.b ∨ λ ^ 2 (see also the result below).

theorem FermatLastTheoremForThreeGen.exists_Solution_of_Solution' {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] {ζ : K} {hζ : IsPrimitiveRoot ζ ↑3} (S' : FermatLastTheoremForThreeGen.Solution' hζ) [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a ∣ b] : ∃ (S₁ : FermatLastTheoremForThreeGen.Solution hζ), S₁.multiplicity = S'.multiplicity

Given S' : Solution', then there is S₁ : Solution such that S₁.multiplicity = S'.multiplicity.