Fermat Last Theorem in the case n = 3
#
The goal of this file is to prove Fermat's Last Theorem in the case n = 3
.
Main results #
fermatLastTheoremThree
: Fermat's Last Theorem forn = 3
: ifa b c : ℕ
are all non-zero thena ^ 3 + b ^ 3 ≠ c ^ 3
.
Implementation details #
We follow the proof in https://webusers.imj-prg.fr/~marc.hindry/Cours-arith.pdf, page 43.
The strategy is the following:
- The so called "Case 1", when
3 ∣ a * b * c
is completely elementary and is proved using congruences modulo9
. - To prove case 2, we consider the generalized equation
a ^ 3 + b ^ 3 = u * c ^ 3
, wherea
,b
, andc
are in the cyclotomic ringℤ[ζ₃]
(whereζ₃
is a primitive cube root of unity) andu
is a unit ofℤ[ζ₃]
.FermatLastTheoremForThree_of_FermatLastTheoremThreeGen
(whose proof is rather elementary on paper) says that to prove Fermat's last theorem for exponent3
, it is enough to prove that this equation has no solutions such thatc ≠ 0
,¬ λ ∣ a
,¬ λ ∣ b
,λ ∣ c
andIsCoprime a b
(where we setλ := ζ₃ - 1
). We call such a tuple aSolution'
. ASolution
is the same as aSolution'
with the additional assumption thatλ ^ 2 ∣ a + b
. We then prove that, givenS' : Solution'
, there isS : Solution
such that the multiplicity ofλ = ζ₃ - 1
inc
is the same inS'
andS
(seeexists_Solution_of_Solution'
). In particular it is enough to prove that noSolution
exists. The key point is a descent argument on the multiplicity ofλ
inc
: starting withS : Solution
we can findS₁ : Solution
with multiplicity strictly smaller (seeexists_Solution_multiplicity_lt
) and this finishes the proof. To constructS₁
we go through aSolution'
and then back to aSolution
. More importantly, we cannot control the unitu
, and this is the reason why we need to consider the generalized equationa ^ 3 + b ^ 3 = u * c ^ 3
. The construction is completely explicit, but it depends crucially onIsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent
, a special case of Kummer's lemma. - Note that we don't prove Case 1 for the generalized equation (in particular we don't prove that
the generalized equation has no nontrivial solutions). This is because the proof, even if
elementary on paper, would be quite annoying to formalize: indeed it involves a lot of explicit
computations in
ℤ[ζ₃] / (λ)
: this ring is isomorphic toℤ / 9ℤ
, but of course, even if we construct such an isomorphism, tactics likedecide
would not work.
To prove Fermat's Last Theorem for n = 3
, it is enough to show 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
.
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.
Instances For
To prove FermatLastTheoremFor 3
, it is enough to prove FermatLastTheoremForThreeGen
.
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.
- u : (NumberField.RingOfIntegers K)ˣ
- hc : self.c ≠ 0
- coprime : IsCoprime self.a self.b
Instances For
Solution
is the same as Solution'
with the additional assumption that λ ^ 2 ∣ a + b
.
- u : (NumberField.RingOfIntegers K)ˣ
- hc : self.c ≠ 0
- coprime : IsCoprime self.a self.b
Instances For
For any S' : Solution'
, the multiplicity of λ
in S'.c
is finite.
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
Instances For
Given S : Solution
, S.multiplicity
is the multiplicity of λ
in S.c
, as a natural
number.
Equations
- S.multiplicity = S.multiplicity
Instances For
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
Instances For
If there is a solution then there is a minimal one.
Given S' : Solution'
, then S'.a
and S'.b
are both congruent to 1
modulo λ ^ 4
or are
both congruent to -1
.
Given S' : Solution'
, we have that 2 ≤ S'.multiplicity
.
Given S : Solution
, we have that 2 ≤ S.multiplicity
.
Given S' : Solution'
, the key factorization of S'.a ^ 3 + S'.b ^ 3
.
Given S' : Solution'
, we have that λ ^ 2
divides one amongst S'.a + S'.b
,
S'.a + η * S'.b
and S'.a + η ^ 2 * S'.b
.
Given S' : Solution'
, we may assume that λ ^ 2
divides S'.a + S'.b ∨ λ ^ 2
(see also the
result below).
Given S' : Solution'
, then there is S₁ : Solution
such that
S₁.multiplicity = S'.multiplicity
.
Given (S : Solution)
, we have that λ ∣ (S.a + η * S.b)
.
Given (S : Solution)
, we have that λ ∣ (S.a + η ^ 2 * S.b)
.
Given (S : Solution)
, we have that λ ^ 2
does not divide S.a + η * S.b
.
Given (S : Solution)
, we have that λ ^ 2
does not divide S.a + η ^ 2 * S.b
.
If p : 𝓞 K
is a prime that divides both S.a + S.b
and S.a + η * S.b
, then p
is associated with λ
.
If p : 𝓞 K
is a prime that divides both S.a + S.b
and S.a + η ^ 2 * S.b
, then p
is associated with λ
.
If p : 𝓞 K
is a prime that divides both S.a + η * S.b
and S.a + η ^ 2 * S.b
, then p
is associated with λ
.
Given S : Solution
, we construct S₁ : Solution'
, with smaller multiplicity of λ
in
c
(see Solution'_descent_multiplicity_lt
below.).
Equations
- One or more equations did not get rendered due to their size.
Instances For
We have that S.Solution'_descent.multiplicity = S.multiplicity - 1
.
We have that S.Solution'_descent.multiplicity < S.multiplicity
.
Given any S : Solution
, there is another S₁ : Solution
such that
S₁.multiplicity < S.multiplicity