Add some lemmas about j-invariant of the Frey curve.

Author: kbuzzard

FLT/Basic/Reductions.lean

@@ -396,6 +396,18 @@ def FreyCurve (P : FreyPackage) : EllipticCurve ℚ := {
         WeierstrassCurve.b₆, WeierstrassCurve.b₈]
       ring }
 
+lemma FreyCurve.j (P : FreyPackage) :
+    P.FreyCurve.j = 2^8*(P.c^(2*P.p)-(P.a*P.b)^P.p)/(P.a*P.b*P.c)^(2*P.p) := by
+  sorry
+
+/-- The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is
+a prime of bad reduction. -/
+lemma FreyCurve.j_valuation_of_bad_prime (P : FreyPackage) {q : ℕ} (hpPrime : q.Prime)
+    (hpbad : (q : ℤ) ∣ P.a * P.b * P.c) (hpodd : 2 < q) :
+    (P.p : ℤ) ∣ padicValRat q P.FreyCurve.j := by
+  sorry
+
+
 end FreyPackage
 
 

blueprint/src/chapter/ch03frey.tex

@@ -215,13 +215,17 @@ \section{Hardly ramified representations}
 If however $p$ divides $abc$ then $E$ has multiplicative 
 reduction at $p$, and we can use the theory of the Tate curve to analyse $\rho$ at $p$.
 
-\begin{theorem}\label{Frey_curve_j}\uses{FLT.FreyCurve} If $(a,b,c,\ell)$ is a Frey package then the $j$-invariant of the corresponding Frey curve is $2^8(C^2-AB)^3/A^2B^2C^2$, where $A=a^\ell$, $B=b^\ell$ and $C=c^\ell$.
+\begin{theorem}\label{Frey_curve_j}\lean{FLT.FreyPackage.FreyCurve.j}\uses{FLT.FreyCurve} If $(a,b,c,\ell)$ is a Frey package then the $j$-invariant of the corresponding Frey curve is $2^8(C^2-AB)^3/A^2B^2C^2$, where $A=a^\ell$, $B=b^\ell$ and $C=c^\ell$.
 \end{theorem}
 \begin{proof}
   Apply the explicit formula (presumably already in mathlib)
 \end{proof}
 
-\begin{corollary}\label{Frey_curve_val_j} If $(a,b,c,\ell)$ is a Frey package and the $j$-invariant of the corresponding Frey curve is $j$, and if $2<p\mid abc$, then the $p$-adic valuation $v_p(j)$ of $j$ is a multiple of $\ell$.
+\begin{corollary}
+  \label{FLT.FreyPackage.FreyCurve.j_valuation_of_bad_prime}
+  \lean{FLT.FreyPackage.FreyCurve.j_valuation_of_bad_prime} 
+  \uses{Frey_curve_j}
+  If $(a,b,c,\ell)$ is a Frey package and the $j$-invariant of the corresponding Frey curve is $j$, and if $2<p\mid abc$, then the $p$-adic valuation $v_p(j)$ of $j$ is a multiple of $\ell$.
 \end{corollary}
 \begin{proof}\uses{Frey_curve_j} Indeed $p$ does not divide $2^8$ as $p>2$, and (using the notation of the previous theorem) $p$ does not divide $C^2-AB$ either, because it divides precisely one of $A$, $B$ and $C$. Hence $v_p(j)=-2v_p(a^\ell b^\ell c^\ell)=-2\ell v_p(abc)$ is a multiple of $\ell$.
 \end{proof}