More tidying up reductions.lean

FLT/Basic/Reductions.lean

@@ -3,9 +3,19 @@ import Mathlib.NumberTheory.FLT.Four
 import Mathlib
 
 /-!
-This results shows that Fermat's Last Theorem for positive integers,
-as formulated in the main `FLT.lean` file, follows from the mathlib
-formalisation of Fermat's Last Theorem.
+This file proves the results which reduce Fermat's Last Theorem
+to Mazur's theorem and the Wiles-Taylor-Wiles theorem.
+
+# Main definitions
+
+* `Frey_package` : A Frey Package is the data of nonzero coprime integers
+$$(a,b,c)$$ and a prime $$p ≥ 5$$ such that $$a^p+b^p=c^p$$ and furthermore
+such that $$a$$ is 3 mod 4 and $$b$$ is 0 mod 2.
+
+# Main theorems
+
+* A counterexample to Fermat's Last Theorem gives a Frey Package
+* There is no Frey Package
 -/
 
 theorem PNat.pow_add_pow_ne_pow_of_FermatLastTheorem :
@@ -20,11 +30,10 @@ namespace FLT
 /-!
 
 A *Frey Package* is a 4-tuple (a,b,c,p) of integers
-satisfying some axioms. The axioms imply that all of
-the all the results in section 4.1 of Serre's paper "Sur les
-représentations modulaire de degré 2 de
-$$Gal(\overline{\mathbb{Q}}/\mathbb{Q})$$"
-apply to the choice of solution $$A=a^p$$, $$B=b^p$$ and $$C=-c^p$$ to $$A+B+C=0.$$
+satisfying some axioms (including $$a^p+b^p=c^p$$).
+The axioms imply that all of
+the all the results in section 4.1 of Serre's paper [serre]
+apply to the curve $$Y^2=X(X-a^p)(X+b^p).$$
 -/
 structure Frey_package where
   a : ℤ
@@ -48,7 +57,7 @@ lemma hgcdac (P : Frey_package) : gcd P.a P.c = 1 := by
 lemma hgcdbc (P : Frey_package) : gcd P.b P.c = 1 := by
   sorry -- these should be one issue
 
-/-- The elliptic curve associated to a Frey package. The conditions imposed
+/-! The elliptic curve associated to a Frey package. The conditions imposed
 upon a Frey package guarantee that the running hypotheses in
 Section 4.1 of [Serre] all hold. -/
 def FreyCurve (P : Frey_package) : EllipticCurve ℚ := {
@@ -59,30 +68,32 @@ def FreyCurve (P : Frey_package) : EllipticCurve ℚ := {
     a₆ := 0
     Δ' :=
     ⟨- (P.a ^ P.p) ^ 2 * (P.b ^ P.p) ^ 2 * (P.c ^ P.p) ^ 2 / 2 ^ 8, -- or whatever it comes out to be with Lean's conventions
-           sorry, -- whatever 1 / the right answer is,
-           sorry, sorry⟩
-    coe_Δ' := sorry -- this should be an issue.
+      sorry, -- whatever 1 / the right answer is,
+      sorry, sorry⟩ -- unwise to embark on these until `coe_Δ'` is proved
+    coe_Δ' := sorry -- check that the discriminant is correctly computed.
   }
 
 /-- There is no Frey package. -/
 theorem false (P : Frey_package) : False := by
   /- Let E be the global minimal model of the corresponding
     Frey curve. -/
   let E : EllipticCurve ℚ := FreyCurve P
-  let G : Type := sorry -- Gal(Q-bar/Q)
-  let i : Group G := sorry
+  let K : Type := sorry -- alg closure of ℚ
+  let i : Field K := sorry
+  let i : Algebra ℚ K := sorry
   let V : Type := sorry -- E[p]
   let i : AddCommGroup V := sorry
   let i : Module (ZMod P.p) V := sorry
-  let ρ : Representation (ZMod P.p) G V := sorry -- action of G on E[p]
+  let ρ : Representation (ZMod P.p) (K ≃ₗ[ℚ] K) V := sorry -- action of G on E[p]
   sorry -- case split on whether ρ is reducible or not.
-
+  -- Then Mazur's theorem shows reducible case is impossible
+  -- and Ribet's theorem shows irreducible case is impossible
 end Frey_package
 
 theorem FermatLastTheorem.of_prime_ge_5 (p : ℕ) (hp₁ : p.Prime) (hp₂ : p ≥ 5) :
     FermatLastTheoremFor p := by
-  -- need to make a Frey package and then use no_Frey_package
-
+  -- assume a counterexample, make a Frey package
+  -- and then use Frey_package → False
   sorry
 
 theorem Wiles_Taylor_Wiles : FermatLastTheorem := by
@@ -91,7 +102,7 @@ theorem Wiles_Taylor_Wiles : FermatLastTheorem := by
   by_cases h : p = 3
   · cases h
     -- ⊢ FermatLastTheoremFor 3
-    sorry -- issue
+    sorry
   · apply FermatLastTheorem.of_prime_ge_5 p hp₁
     by_contra h2
     push_neg at h2