The first case of Fermat's Last Theorem for regular primes

This file proves the first case of Fermat's Last Theorem for regular primes, reducing the final statement to a normalized version and establishing the required cyclotomic ideal factorization.

def FltRegular.CaseI.SlightlyEasier : Prop

Statement of case I with additional assumptions.

Equations

• FltRegular.CaseI.SlightlyEasier = ∀ ⦃a b c : ℤ⦄ {p : ℕ} [Fact (Nat.Prime p)], IsRegularPrime p → 5 ≤ p → {a, b, c}.gcd id = 1 → ¬a ≡ b [ZMOD ↑p] → ¬↑p ∣ a * b * c → a ^ p + b ^ p ≠ c ^ p

def FltRegular.CaseI.Statement : Prop

Statement of case I.

Equations

• FltRegular.CaseI.Statement = ∀ ⦃a b c : ℤ⦄ {p : ℕ} [Fact (Nat.Prime p)], IsRegularPrime p → ¬↑p ∣ a * b * c → a ^ p + b ^ p ≠ c ^ p

theorem FltRegular.CaseI.may_assume : SlightlyEasier → Statement

It suffices to prove Case I under the additional normalized hypotheses.

theorem FltRegular.ab_coprime {p : ℕ} {a b c : ℤ} (H : a ^ p + b ^ p = c ^ p) (hpzero : p ≠ 0) (hgcd : {a, b, c}.gcd id = 1) : IsCoprime a b

In a normalized Fermat solution, a and b are coprime.

theorem FltRegular.is_principal_aux {p : ℕ} {K' : Type u_1} [Field K'] [CharZero K'] [IsCyclotomicExtension {p} ℚ K'] [Fintype (ClassGroup (NumberField.RingOfIntegers K'))] {a b : ℤ} {ζ : NumberField.RingOfIntegers K'} (hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K')))) {I : Ideal (NumberField.RingOfIntegers K')} (hI : Ideal.span {↑a + ζ * ↑b} = I ^ p) : ∃ (u : (NumberField.RingOfIntegers K')ˣ) (α : NumberField.RingOfIntegers K'), ↑u * α ^ p = ↑a + ζ * ↑b

A p-th-power principal ideal has a generator that is a unit times a p-th power.

theorem FltRegular.instNeZeroNat_leanPool {p : ℕ} [hpri : Fact (Nat.Prime p)] : NeZero p

theorem FltRegular.instIsCyclotomicExtensionSingletonNatSetRatCyclotomicField_leanPool {p : ℕ} [hpri : Fact (Nat.Prime p)] : IsCyclotomicExtension {p} ℚ (CyclotomicField p ℚ)

theorem FltRegular.instIsCyclotomicExtensionSingletonNatSetIntRingOfIntegersCyclotomicFieldRat_leanPool {p : ℕ} [hpri : Fact (Nat.Prime p)] : IsCyclotomicExtension {p} ℤ (NumberField.RingOfIntegers (CyclotomicField p ℚ))

theorem FltRegular.exists_ideal {p : ℕ} [hpri : Fact (Nat.Prime p)] {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) (hgcd : {a, b, c}.gcd id = 1) (caseI : ¬↑p ∣ a * b * c) {ζ : NumberField.RingOfIntegers (CyclotomicField p ℚ)} (hζ : ζ ∈ Polynomial.nthRootsFinset p 1) : ∃ (I : Ideal (NumberField.RingOfIntegers (CyclotomicField p ℚ))), Ideal.span {↑a + ζ * ↑b} = I ^ p

The cyclotomic ideal generated by a + ζ * b is a p-th power.

theorem FltRegular.is_principal {p : ℕ} [hpri : Fact (Nat.Prime p)] {a b c : ℤ} {ζ : NumberField.RingOfIntegers (CyclotomicField p ℚ)} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p) (hgcd : {a, b, c}.gcd id = 1) (caseI : ¬↑p ∣ a * b * c) (H : a ^ p + b ^ p = c ^ p) (hζ : IsPrimitiveRoot ζ p) : ∃ (u : (NumberField.RingOfIntegers (CyclotomicField p ℚ))ˣ) (α : NumberField.RingOfIntegers (CyclotomicField p ℚ)), ↑u * α ^ p = ↑a + ζ * ↑b

The cyclotomic factor a + ζ * b is a unit times a p-th power.

theorem FltRegular.ex_fin_div {p : ℕ} [hpri : Fact (Nat.Prime p)] {a b c : ℤ} {ζ : NumberField.RingOfIntegers (CyclotomicField p ℚ)} (hp5 : 5 ≤ p) (hreg : IsRegularPrime p) (hζ : IsPrimitiveRoot ζ p) (hgcd : {a, b, c}.gcd id = 1) (caseI : ¬↑p ∣ a * b * c) (H : a ^ p + b ^ p = c ^ p) : ∃ (k₁ : Fin p) (k₂ : Fin p), ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂

Two exponents whose associated cyclotomic linear combination is divisible by p.

theorem FltRegular.caseI_easier {p : ℕ} [hpri : Fact (Nat.Prime p)] {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p) (hgcd : {a, b, c}.gcd id = 1) (hab : ¬a ≡ b [ZMOD ↑p]) (caseI : ¬↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p

Case I with additional assumptions.

theorem FltRegular.caseI {a b c : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hreg : IsRegularPrime p) (caseI : ¬↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p

Case I.