p-torsion of an elliptic curve as a Galois rep

ImperialCollegeLondon · Mar 23, 2024 · 9dce26e · 9dce26e
1 parent 782a81e
commit 9dce26e
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 10 deletions.
diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean
@@ -392,32 +392,35 @@ def FreyCurve (P : FreyPackage) : EllipticCurve ℚ := {
 end FreyPackage
 
 
-abbrev Qbar := AlgebraicClosure ℚ
 
-open WeierstrassCurve
 
 
 /-!
 
-What can we say about this representation? It follows from a profound theorem
-of Mazur (and much other work) that this representation must be irreducible.
+Given an elliptic curve over `ℚ`, the p-torsion points defined over an algebraic
+closure of `ℚ` are a 2-dimensional Galois reprentation. What can we say about the Galois
+representation attached to the p-torsion of the Frey curve attached to a Frey package?
+
+It follows (after a little work!) from a profound theorem of Mazur that this representation
+must be irreducible.
 
 -/
 
+abbrev Qbar := AlgebraicClosure ℚ
+
+open WeierstrassCurve
 theorem Mazur_Frey (P : FreyPackage) :
-    IsSimpleModule (ZMod P.p)
-    (EllipticCurve.mod_p_Galois_representation P.FreyCurve P.p Qbar).asModule := sorry
+    IsSimpleModule (ZMod P.p) (P.FreyCurve.mod_p_Galois_representation P.p Qbar).asModule := sorry
 
 /-!
 
-But it follows from a profound theorem of Ribet, and the fact (proved by Wiles) that the Frey Curve
-is modular, that the representation cannot be irreducible.
+But it follows from a profound theorem of Ribet, and the even more profound theorem
+(proved by Wiles) that the Frey Curve is modular, that the representation cannot be irreducible.
 
 -/
 
 theorem Wiles_Frey (P : FreyPackage) :
-    ¬ IsSimpleModule (ZMod P.p)
-        (EllipticCurve.mod_p_Galois_representation P.FreyCurve P.p Qbar).asModule := sorry
+    ¬ IsSimpleModule (ZMod P.p) (P.FreyCurve.mod_p_Galois_representation P.p Qbar).asModule := sorry
 
 /-!
 

diff --git a/FLT/EllipticCurve/Torsion.lean b/FLT/EllipticCurve/Torsion.lean
@@ -29,6 +29,10 @@ abbrev EllipticCurve.n_torsion (n : ℕ) : Type u := Submodule.torsionBy ℤ (E.
 --variable (n : ℕ) in
 --#synth AddCommGroup (E.n_torsion n)
 
+def ZMod.module (A : Type*) [AddCommGroup A] (n : ℕ) (hn : ∀ a : A, n • a = 0) :
+    Module (ZMod n) A :=
+  sorry
+
 -- not sure if this instance will cause more trouble than it's worth
 instance (n : ℕ) : Module (ZMod n) (E.n_torsion n) := sorry -- shouldn't be too hard