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 whenn = 3
: ifa b c : ℤ
are such that¬ 3 ∣ a * b * c
, thena ^ 3 + b ^ 3 ≠ c ^ 3
.
TODO #
Prove case 2.
Implementation details #
We follow the proof in https://webusers.imj-prg.fr/~marc.hindry/Cours-arith.pdf, page 43. The The strategy is the following:
- Case 1 is completely elementary and is proved using congruences modulo
9
. - 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
. 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 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
.
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
.
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).get ⋯
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 λ
.