From f2ac078cf46f48158b5a58b9e8a2eed0b7eb93a2 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 14 Dec 2023 19:06:01 +0000 Subject: [PATCH 1/8] remove file which should never have been committed --- blueprint/src/web.log | 312 ------------------------------------------ 1 file changed, 312 deletions(-) delete mode 100644 blueprint/src/web.log diff --git a/blueprint/src/web.log b/blueprint/src/web.log deleted file mode 100644 index a226bde2..00000000 --- a/blueprint/src/web.log +++ /dev/null @@ -1,312 +0,0 @@ -This is XeTeX, Version 3.141592653-2.6-0.999993 (TeX Live 2022/dev/Debian) (preloaded format=xelatex 2023.5.31) 15 NOV 2023 18:51 -entering extended mode - restricted \write18 enabled. - %&-line parsing enabled. -**web.tex -(./web.tex -LaTeX2e <2021-11-15> patch level 1 -L3 programming layer <2022-01-21> -(/usr/share/texlive/texmf-dist/tex/latex/base/report.cls -Document Class: report 2021/10/04 v1.4n Standard LaTeX document class -(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo -File: size10.clo 2021/10/04 v1.4n Standard LaTeX file (size option) -) -\c@part=\count181 -\c@chapter=\count182 -\c@section=\count183 -\c@subsection=\count184 -\c@subsubsection=\count185 -\c@paragraph=\count186 -\c@subparagraph=\count187 -\c@figure=\count188 -\c@table=\count189 -\abovecaptionskip=\skip47 -\belowcaptionskip=\skip48 -\bibindent=\dimen138 -) -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty -Package: amsmath 2021/10/15 v2.17l AMS math features -\@mathmargin=\skip49 - -For additional information on amsmath, use the `?' option. -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty -Package: amstext 2021/08/26 v2.01 AMS text - -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty -File: amsgen.sty 1999/11/30 v2.0 generic functions -\@emptytoks=\toks16 -\ex@=\dimen139 -)) -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty -Package: amsbsy 1999/11/29 v1.2d Bold Symbols -\pmbraise@=\dimen140 -) -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty -Package: amsopn 2021/08/26 v2.02 operator names -) -\inf@bad=\count190 -LaTeX Info: Redefining \frac on input line 234. -\uproot@=\count191 -\leftroot@=\count192 -LaTeX Info: Redefining \overline on input line 399. -\classnum@=\count193 -\DOTSCASE@=\count194 -LaTeX Info: Redefining \ldots on input line 496. -LaTeX Info: Redefining \dots on input line 499. -LaTeX Info: Redefining \cdots on input line 620. -\Mathstrutbox@=\box50 -\strutbox@=\box51 -\big@size=\dimen141 -LaTeX Font Info: Redeclaring font encoding OML on input line 743. -LaTeX Font Info: Redeclaring font encoding OMS on input line 744. -\macc@depth=\count195 -\c@MaxMatrixCols=\count196 -\dotsspace@=\muskip16 -\c@parentequation=\count197 -\dspbrk@lvl=\count198 -\tag@help=\toks17 -\row@=\count199 -\column@=\count266 -\maxfields@=\count267 -\andhelp@=\toks18 -\eqnshift@=\dimen142 -\alignsep@=\dimen143 -\tagshift@=\dimen144 -\tagwidth@=\dimen145 -\totwidth@=\dimen146 -\lineht@=\dimen147 -\@envbody=\toks19 -\multlinegap=\skip50 -\multlinetaggap=\skip51 -\mathdisplay@stack=\toks20 -LaTeX Info: Redefining \[ on input line 2938. -LaTeX Info: Redefining \] on input line 2939. -) -(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty -Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support -\symAMSa=\mathgroup4 -\symAMSb=\mathgroup5 -LaTeX Font Info: Redeclaring math symbol \hbar on input line 98. -LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' -(Font) U/euf/m/n --> U/euf/b/n on input line 106. -) -(/usr/share/texlive/texmf-dist/tex/latex/amscls/amsthm.sty -Package: amsthm 2020/05/29 v2.20.6 -\thm@style=\toks21 -\thm@bodyfont=\toks22 -\thm@headfont=\toks23 -\thm@notefont=\toks24 -\thm@headpunct=\toks25 -\thm@preskip=\skip52 -\thm@postskip=\skip53 -\thm@headsep=\skip54 -\dth@everypar=\toks26 -) -(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty -Package: amssymb 2013/01/14 v3.01 AMS font symbols -) -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty -Package: hyperref 2021-06-07 v7.00m Hypertext links for LaTeX - -(/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty -Package: ltxcmds 2020-05-10 v1.25 LaTeX kernel commands for general use (HO) -) -(/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty -Package: iftex 2020/03/06 v1.0d TeX engine tests -) -(/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty -Package: pdftexcmds 2020-06-27 v0.33 Utility functions of pdfTeX for LuaTeX (HO -) - -(/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty -Package: infwarerr 2019/12/03 v1.5 Providing info/warning/error messages (HO) -) -Package pdftexcmds Info: \pdf@primitive is available. -Package pdftexcmds Info: \pdf@ifprimitive is available. -Package pdftexcmds Info: \pdfdraftmode not found. -) -(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty -Package: keyval 2014/10/28 v1.15 key=value parser (DPC) -\KV@toks@=\toks27 -) -(/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty -Package: kvsetkeys 2019/12/15 v1.18 Key value parser (HO) -) -(/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty -Package: kvdefinekeys 2019-12-19 v1.6 Define keys (HO) -) -(/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty -Package: pdfescape 2019/12/09 v1.15 Implements pdfTeX's escape features (HO) -) -(/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty -Package: hycolor 2020-01-27 v1.10 Color options for hyperref/bookmark (HO) -) -(/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty -Package: letltxmacro 2019/12/03 v1.6 Let assignment for LaTeX macros (HO) -) -(/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty -Package: auxhook 2019-12-17 v1.6 Hooks for auxiliary files (HO) -) -(/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty -Package: kvoptions 2020-10-07 v3.14 Key value format for package options (HO) -) -\@linkdim=\dimen148 -\Hy@linkcounter=\count268 -\Hy@pagecounter=\count269 - -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def -File: pd1enc.def 2021-06-07 v7.00m Hyperref: PDFDocEncoding definition (HO) -) -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref-langpatches.def -File: hyperref-langpatches.def 2021-06-07 v7.00m Hyperref: patches for babel la -nguages -) -(/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty -Package: intcalc 2019/12/15 v1.3 Expandable calculations with integers (HO) -) -(/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty -Package: etexcmds 2019/12/15 v1.7 Avoid name clashes with e-TeX commands (HO) -) -\Hy@SavedSpaceFactor=\count270 - -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def -File: puenc.def 2021-06-07 v7.00m Hyperref: PDF Unicode definition (HO) -) -Package hyperref Info: Hyper figures OFF on input line 4192. -Package hyperref Info: Link nesting OFF on input line 4197. -Package hyperref Info: Hyper index ON on input line 4200. -Package hyperref Info: Plain pages OFF on input line 4207. -Package hyperref Info: Backreferencing OFF on input line 4212. -Package hyperref Info: Implicit mode ON; LaTeX internals redefined. -Package hyperref Info: Bookmarks ON on input line 4445. -\c@Hy@tempcnt=\count271 - -(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty -\Urlmuskip=\muskip17 -Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. -) -LaTeX Info: Redefining \url on input line 4804. -\XeTeXLinkMargin=\dimen149 - -(/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty -Package: bitset 2019/12/09 v1.3 Handle bit-vector datatype (HO) - -(/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty -Package: bigintcalc 2019/12/15 v1.5 Expandable calculations on big integers (HO -) -)) -\Fld@menulength=\count272 -\Field@Width=\dimen150 -\Fld@charsize=\dimen151 -Package hyperref Info: Hyper figures OFF on input line 6076. -Package hyperref Info: Link nesting OFF on input line 6081. -Package hyperref Info: Hyper index ON on input line 6084. -Package hyperref Info: backreferencing OFF on input line 6091. -Package hyperref Info: Link coloring OFF on input line 6096. -Package hyperref Info: Link coloring with OCG OFF on input line 6101. -Package hyperref Info: PDF/A mode OFF on input line 6106. -LaTeX Info: Redefining \ref on input line 6146. -LaTeX Info: Redefining \pageref on input line 6150. - -(/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty -Package: atbegshi-ltx 2021/01/10 v1.0c Emulation of the original atbegshi -package with kernel methods -) -\Hy@abspage=\count273 -\c@Item=\count274 -\c@Hfootnote=\count275 -) -Package hyperref Info: Driver (autodetected): hxetex. - -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hxetex.def -File: hxetex.def 2021-06-07 v7.00m Hyperref driver for XeTeX - -(/usr/share/texlive/texmf-dist/tex/generic/stringenc/stringenc.sty -Package: stringenc 2019/11/29 v1.12 Convert strings between diff. encodings (HO -) -) -\pdfm@box=\box52 -\c@Hy@AnnotLevel=\count276 -\HyField@AnnotCount=\count277 -\Fld@listcount=\count278 -\c@bookmark@seq@number=\count279 - -(/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty -Package: rerunfilecheck 2019/12/05 v1.9 Rerun checks for auxiliary files (HO) - -(/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty -Package: atveryend-ltx 2020/08/19 v1.0a Emulation of the original atveryend pac -kage -with kernel methods -) -(/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty -Package: uniquecounter 2019/12/15 v1.4 Provide unlimited unique counter (HO) -) -Package uniquecounter Info: New unique counter `rerunfilecheck' on input line 2 -86. -) -\Hy@SectionHShift=\skip55 -) -(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty -Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR) - -(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty -Package: graphics 2021/03/04 v1.4d Standard LaTeX Graphics (DPC,SPQR) - -(/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty -Package: trig 2021/08/11 v1.11 sin cos tan (DPC) -) -(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg -File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration -) -Package graphics Info: Driver file: xetex.def on input line 107. - -(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/xetex.def -File: xetex.def 2021/03/18 v5.0k Graphics/color driver for xetex -)) -\Gin@req@height=\dimen152 -\Gin@req@width=\dimen153 -) -(/usr/share/texlive/texmf-dist/tex/latex/cleveref/cleveref.sty -Package: cleveref 2018/03/27 v0.21.4 Intelligent cross-referencing -Package cleveref Info: `hyperref' support loaded on input line 2370. -LaTeX Info: Redefining \cref on input line 2370. -LaTeX Info: Redefining \Cref on input line 2370. -LaTeX Info: Redefining \crefrange on input line 2370. -LaTeX Info: Redefining \Crefrange on input line 2370. -LaTeX Info: Redefining \cpageref on input line 2370. -LaTeX Info: Redefining \Cpageref on input line 2370. -LaTeX Info: Redefining \cpagerefrange on input line 2370. -LaTeX Info: Redefining \Cpagerefrange on input line 2370. -LaTeX Info: Redefining \labelcref on input line 2370. -LaTeX Info: Redefining \labelcpageref on input line 2370. -Package cleveref Info: `amsthm' support loaded on input line 3026. -Package cleveref Info: always capitalise cross-reference names on input line 78 -30. -Package cleveref Info: always capitalise cross-reference names on input line 78 -52. -) - -! LaTeX Error: File `blueprint.sty' not found. - -Type X to quit or to proceed, -or enter new name. (Default extension: sty) - -Enter file name: -! Emergency stop. - - -l.11 ^^M - -End of file on the terminal! - - -Here is how much of TeX's memory you used: - 9289 strings out of 476191 - 140149 string characters out of 5812072 - 492326 words of memory out of 5000000 - 29969 multiletter control sequences out of 15000+600000 - 469627 words of font info for 30 fonts, out of 8000000 for 9000 - 1348 hyphenation exceptions out of 8191 - 60i,0n,64p,222b,40s stack positions out of 5000i,500n,10000p,200000b,80000s -No pages of output. From 5c8a683168a01922e61443373c5ee991909a91f6 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 14 Dec 2023 19:10:43 +0000 Subject: [PATCH 2/8] add stub HardlyRamified file --- FLT/Basic/HardlyRamified.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 FLT/Basic/HardlyRamified.lean diff --git a/FLT/Basic/HardlyRamified.lean b/FLT/Basic/HardlyRamified.lean new file mode 100644 index 00000000..163e131c --- /dev/null +++ b/FLT/Basic/HardlyRamified.lean @@ -0,0 +1,13 @@ +import Mathlib.Tactic + +/- +Taylor: You could say that +a representation + +r: G_Q -> GL_2(F_p) + +is *hardly ramified* if 1) det = cyclo, 2) unramified outside 2p, 3) +r|_{G_p} comes from ffgs and r|_{G_2}^ss is unramified. + +Theorem: p-torsion in Frey curve is hardly ramified. +-/ From a0cc286368cf801c1b018f29caa29f68900aea13 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 14 Dec 2023 19:11:23 +0000 Subject: [PATCH 3/8] update stub Tate curve file --- FLT/TateCurve.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/FLT/TateCurve.lean b/FLT/TateCurve.lean index a8e0781c..f1b1313b 100644 --- a/FLT/TateCurve.lean +++ b/FLT/TateCurve.lean @@ -4,6 +4,14 @@ Need Tate uniformisation from Silverman 2 Ch 5. Don't need surjectivity. May as well work over a general field complete wrt a nontrivial nonarch norm. Key result needed: Galois action on Qpbar-points of p-torsion of elliptic curve E -is isomorphic to some explicit quotient of Qpbar^* by q(E)^ℤ. +over Qp is isomorphic to some explicit quotient of Qpbar^* by q(E)^ℤ. +One of the hardest parts of the argument is surjectivity; we don't need it so I propose +we skip it. This enables the entire argument to be run over a field complete with respect +to a nontrivial nonarchimedean real-valued norm. + +Key thing we want: injection from K^* / into E(K) where K is a field complete wrt +a nontriv nonarch norm, E is the Frey curve and q is chosen appropriately; proof that the injection is functorial in the sense that if K -> L +is an injection of fields and the norm on L restricts to the norm on K then the obvious +diagram commutes. -/ From d86512fe74f772b111299d4887ef47e32e7416f6 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 14 Dec 2023 19:15:44 +0000 Subject: [PATCH 4/8] update mathlib --- lake-manifest.json | 36 ------------------------------------ 1 file changed, 36 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 55c90df4..e16adec1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -54,42 +54,6 @@ "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/xubaiw/CMark.lean", - "type": "git", - "subDir": null, - "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", - "name": "CMark", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/hargonix/LeanInk", - "type": "git", - "subDir": null, - "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", - "name": "leanInk", - "manifestFile": "lake-manifest.json", - "inputRev": "doc-gen", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "rev": "3cc5df1be7f6db5ac13f26edda3fc258e199ab5f", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, "configFile": "lakefile.lean"}], "name": "FLT", "lakeDir": ".lake"} From f93abe0174017d1d1c76b68aab25ea16862acda1 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 14 Dec 2023 20:18:03 +0000 Subject: [PATCH 5/8] add lean copilot --- lake-manifest.json | 9 +++++++++ lakefile.lean | 4 ++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e16adec1..ae456b96 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -54,6 +54,15 @@ "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/lean-dojo/LeanCopilot", + "type": "git", + "subDir": null, + "rev": "7f053194ba41581ab110232a1f8aa295cbddbd5c", + "name": "LeanCopilot", + "manifestFile": "lake-manifest.json", + "inputRev": "v1.0.0", + "inherited": false, "configFile": "lakefile.lean"}], "name": "FLT", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 8948fcbb..e91024c9 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -24,8 +24,8 @@ def weakLeanArgs : Array String := package FLT where moreServerArgs := moreServerArgs -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" +require mathlib from git "https://github.com/leanprover-community/mathlib4.git" +require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot" @ "v1.0.0" -- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen meta if get_config? env = some "dev" then From cd83088ed649ffe4b2a23c0992585077a998a85e Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 14 Dec 2023 22:35:12 +0000 Subject: [PATCH 6/8] update reductions.tex (get colours right) --- blueprint/src/chapter/reductions.tex | 41 ++++++++++++++++------------ 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/blueprint/src/chapter/reductions.tex b/blueprint/src/chapter/reductions.tex index 86d403e6..df2e2011 100644 --- a/blueprint/src/chapter/reductions.tex +++ b/blueprint/src/chapter/reductions.tex @@ -27,9 +27,9 @@ \section{Reduction to \texorpdfstring{$n\geq5$}{ngeq5} and prime} The proof has been formalised in Lean in the FLT-regular project \href{https://github.com/leanprover-community/flt-regular/blob/861b7df057140b45b8bb7d30d33426ffbbdda52b/FltRegular/FltThree/FltThree.lean#L698}{\color{blue}\underline{here}}. To get this node green, the proof (or another proof) needs to be upstreamed to mathlib. \end{proof} -\begin{corollary}\label{WLOG_p_ge_5}\uses{p_not_three, WLOG_n_prime}\leanok If there is a counterexample to Fermat's Last Theorem, then there is a counterexample $a^p+b^p=c^p$ with $p$ prime and $p\geq 5$. +\begin{corollary}\label{WLOG_p_ge_5}\leanok If there is a counterexample to Fermat's Last Theorem, then there is a counterexample $a^p+b^p=c^p$ with $p$ prime and $p\geq 5$. \end{corollary} -\begin{proof}\leanok Follows from the previous two lemmas.\end{proof} +\begin{proof}\uses{p_not_three, WLOG_n_prime}\leanok Follows from the previous two lemmas.\end{proof} \section{Frey packages} @@ -39,16 +39,16 @@ \section{Frey packages} Our next reduction is as follows: -\begin{lemma}\label{Frey_package_of_FLT_counterex}\lean{FLT.FreyPackage.of_not_FermatLastTheorem}\uses{Frey_package, WLOG_p_ge_5}\leanok +\begin{lemma}\label{Frey_package_of_FLT_counterex}\lean{FLT.FreyPackage.of_not_FermatLastTheorem}\leanok If Fermat's Last Theorem is false, then there exists a Frey package. \end{lemma} -\begin{proof} By Corollary \ref{WLOG_p_ge_5} we may assume that there is a counterexample $x^p+y^p=z^p$ with $p\geq 5$ and prime; we now build a Frey package from this data. +\begin{proof}\uses{Frey_package, WLOG_p_ge_5} By Corollary \ref{WLOG_p_ge_5} we may assume that there is a counterexample $x^p+y^p=z^p$ with $p\geq 5$ and prime; we now build a Frey package from this data. If the greatest common divisor of $x,y,z$ is $d$ then $x^p+y^p=z^p$ implies $(x/d)^p+(y/d)^p=(z/d)^p$. Dividing through, we can thus assume that no prime divides all of $x,y,z$. Under this assumption we must have that $x,y,z$ are pairwise coprime, as if some prime divides two of the integers $x,y,z$ then by $x^p+y^p=z^p$ and unique factorization it must divide all three of them. In particular we may assume that not all of $x,y,z$ are even, and now reducing modulo~2 shows that precisely one of them must be even. Next we show that we can find a counterexample with $y$ even. Indeed, if $x$ is even then we can switch $x$ and $y$, and if $z$ is even then we can replace $z$ by $-y$ and $y$ by $-z$ (using that $p$ is odd). - The last thing to ensure is that $x$ is 3 mod~4. We know that $x$ is odd, so it is either 1 or~3 mod~4. If $x$ is 3 mod~4 then we are home; if however $x$ is 1 mod~4 we replace $x,y,z$ by their negatives and this is the Frey package we seek. + The last thing to ensure is that $x$ is 3 mod~4. We know that $x$ is odd, so it is either~1 or~3 mod~4. If $x$ is 3 mod~4 then we are home; if however $x$ is 1 mod~4 we replace $x,y,z$ by their negatives and this is the Frey package we seek. \end{proof} \section{Galois representations and elliptic curves} @@ -59,29 +59,34 @@ \section{Galois representations and elliptic curves} The group structure behaves well under change of field: If $K$ and $L$ are two fields of characteristic zero and $f:K\to L$ is a field homomorphism, the map from $E(K)$ to $E(L)$ induced by $f$ is an additive group homomorphism. This construction is functorial (it sends the identity to the identity, and compositions to compositions). Thus if $f$ is an isomorphism, then the induced map $E(K)\to E(L)$ is also an isomorphism, with the inverse morphism being the map $E(L)\to E(K)$ induced by $f^{-1}$. This construction thus gives us an action of the multiplicative group $\Aut(K)$ of automorphisms of the field $K$ on the additive abelian group $E(K)$. In particular, if $\Qbar$ denotes an algebraic closure of the rationals (for example, the algebraic numbers in $\bbC$) and if $\GQ$ denotes the group of field isomorphisms $\Qbar\to\Qbar$, then for any elliptic curve $E$ over $\Q$ we have an action of $\GQ$ on the additive abelian group $E(\Qbar)$. -If $A$ is any additive abelian group, and if $p$ is a prime number, then the subgroup $A[p]$ of elements $a$ such that $pa=0$ is naturally a vector space over the field $\Z/p\Z$. If a group is acting on $A$ via additive group isomorphisms, then there will be an induced action of the group on $A[p]$, which thus inherits the stucture of a mod $p$ representation of $G$. Applying this to the above situation, -if $E$ is an elliptic curve over $\Q$ then $\GQ$ acts on $E(\Qbar)[p]$ and this is the \emph{mod $p$ Galois representation} attached to -the curve $E$. +We need a variant of this construction where we only consider the $p$-torsion of the curve. Recall that if $A$ is any additive abelian group, and if $p$ is a prime number, then the subgroup $A[p]$ of elements $a$ such that $pa=0$ is naturally a vector space over the field $\Z/p\Z$. If a group is acting on $A$ via additive group isomorphisms, then there will be an induced action of the group on $A[p]$, which thus inherits the stucture of a mod $p$ representation of $G$. Applying this to the above situation, we deduce that if $E$ is an elliptic curve over $\Q$ then $\GQ$ acts on $E(\Qbar)[p]$ and this is the \emph{mod $p$ Galois representation} attached to the curve $E$. -\begin{definition}[Frey]\label{Frey_curve}\lean{FLT.FreyCurve}\uses{Frey_package} Given a Frey package $(a,b,c,p)$, the corresponding \emph{Frey curve} (considered by Frey and, before him, Hellgouarch) is the elliptic curve $E$ defined by the equation $Y^2=X(X-a^p)(X+b^p)$\end{definition} +In the next section we explain which elliptic curve we will use. -Note that the roots of the cubic $X(X-a^p)(X+b^p)$ are distinct because $a,b,c$ are nonzero, and thus the Frey curve is an -elliptic curve over $\Q$. +\section{The Frey curve} + +\begin{stealthdefinition}[Frey] + Given a Frey package $(a,b,c,p)$, the corresponding \emph{Frey curve} (considered by Frey and, before him, Hellegouarch) is the elliptic curve $E$ defined by the equation $Y^2=X(X-a^p)(X+b^p)$\end{definition} + +\begin{theorem}\label{Frey_curve}\lean{FLT.FreyCurve} + The Frey curve is an elliptic curve over $\Q$. +\end{theorem} +\begin{proof}\uses{Frey_package} Indeed, the roots of the cubic $X(X-a^p)(X+b^p)$ are distinct because $a,b,c$ are nonzero and $a^p+b^p=c^p$. +\end{proof} \begin{definition}[mod $p$ Galois representation attached to a Frey package]\label{Frey_mod_p_Galois_representation}\lean{FLT.FreyCurve.mod_p_Galois_representation}\uses{Frey_curve} Given a Frey package $(a,b,c,p)$ with corresponding Frey curve $E$, the mod $p$ Galois representation associated to this package is the representation of $\GQ$ on $E(\Qbar)[p].$\end{definition} +Frey's observation is that this mod $p$ Galois representation has some very surprising properties. We will come back to this in the next chapter. + +\section{Reduction to two big theorems.} + Recall that a representation of a group $G$ on a vector space $W$ is said to be \emph{irreducible} if there are precisely two $G$-stable subspaces of $W$, namely $0$ and $W$. The representation is said to be \emph{reducible} otherwise. -Now say Fermat's Last Theorem is false, and hence by Lemma~\ref{Frey_package_of_FLT_counterex} a Frey package $(a,b,c,p)$ exists. Consider the mod $p$ representation of $\GQ$ coming from the $p$-torsion in the Frey curve $Y^2=X(x-a^p)(X+b^p)$ -associated to the package. Let's call this representation $\rho$. Is it reducible or irreducible? +Now say Fermat's Last Theorem is false, and hence by Lemma~\ref{Frey_package_of_FLT_counterex} a Frey package $(a,b,c,p)$ exists. Consider the mod $p$ representation of $\GQ$ coming from the $p$-torsion in the Frey curve $Y^2=X(x-a^p)(X+b^p)$ associated to the package. Let's call this representation $\rho$. Is it reducible or irreducible? \begin{theorem}[Mazur]\label{Mazur_on_Frey_curve}\lean{FLT.FreyCurve.Mazur_Frey}\uses{Frey_mod_p_Galois_representation}\leanok $\rho$ cannot be reducible.\end{theorem} -\begin{proof}\tangled This follows from a profound result of Mazur \cite{mazur} from 1979, which boils down to the fact that the torsion subgroup of an elliptic curve over $\Q$ can have size at most~16. In fact some work still needs to be done to deduce the theorem from Mazur's result. We omit the argument for now -- it is explained in Proposition~6 of~\cite{serreconj}. The reduction to Mazur's theorem -needs the theory of the Tate curve (concrete p-adic uniformisation of elliptic curves) and also some of the theory of finite flat group schemes (or the theory of the canonical subgroup), so in particular even the reduction to Mazur's theorem is a lot of hard work. -Mazur's theorem itself is of course way more difficult, and right now nobody is working on a formalisation (it would be a substantial -project in itself). +\begin{proof}\tangled This follows from a profound result of Mazur \cite{mazur} from 1979, which boils down to the fact that the torsion subgroup of an elliptic curve over $\Q$ can have size at most~16. In fact a fair amount of work needs to be done to deduce the theorem from Mazur's result. We omit the reduction for now -- it is explained in Proposition~6 of~\cite{serreconj}. In brief, it uses the theory of the Tate curve (concrete p-adic uniformisation of elliptic curves) and also some of the theory of finite flat group schemes (or the theory of the canonical subgroup). Mazur's theorem itself is of course way more difficult, and right now nobody is working on a formalisation as far as I know (it would be a substantial project in itself). \end{proof} -{\bf TODO two rferences above} \begin{theorem}[Wiles,Taylor--Wiles]\label{Wiles_on_Frey_curve}\lean{FLT.FreyCurve.Wiles_Frey}\uses{Frey_mod_p_Galois_representation}\leanok $\rho$ cannot be irreducible either.\end{theorem} \begin{proof}\tangled This is the main content of Wiles' magnum opus. We omit the argument for now, although later on in this project we will have a lot to say about a proof of this. From 328d4dcc97125854b812ff615678f7c96f66dee3 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 14 Dec 2023 22:35:24 +0000 Subject: [PATCH 7/8] Add beginnings of chapter on Frey curves --- blueprint/src/chapter/frey.tex | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 blueprint/src/chapter/frey.tex diff --git a/blueprint/src/chapter/frey.tex b/blueprint/src/chapter/frey.tex new file mode 100644 index 00000000..41a0d7f2 --- /dev/null +++ b/blueprint/src/chapter/frey.tex @@ -0,0 +1,23 @@ +\chapter{The Frey Curve} + +\section{Overview} + +In the last chapter we explained how, given a counterexample to Fermat's Last Theorem we could construct a Frey curve, which is an elliptic curve with some interesting properties. Let $\rho:\GQ\to\GL_2(\Z/p\Z)$ be the representation on the $p$-torsion of this curve. In this chapter we discuss some basic properties of this representation, used both by Mazur to prove that $\rho$ cannot be reducible and by Wiles to prove that it can't be irreducible. + +\section{Hardly ramified representations} + +We make the following definition (this is not in the literature but it is a useful concept for us). We discuss the meaning of some of the concepts involved afterwards. + +\begin{stealthdefinition} Let $p\geq5$ be a prime. A representation $\rho: \GQ\to \GL_2(\Z/p\Z)$ is said to be \emph{hardly ramified} if it satisfies the following four axioms: + \begin{enumerate} + \item $\det(\rho)$ is the mod $p$ cyclotomic character; + \item $\rho$ is unramified outside $2p$; + \item The semisimplification of the restriction of $\rho$ to is unramified. + \item The restriction of $\rho$ to $\GQp$ comes from a finite flat group scheme; + \end{enumerate} +\end{stealthdefinition} + +The theorem we want to discuss in this section is: + +\begin{theorem} If $\rho$ is the Galois representation on the $p$-torsion of the Frey curve coming from a Frey package, then $\rho$ is hardly ramified. +\end{theorem} From ee411194cd679e8df3da8cd899f91823382f164c Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 14 Dec 2023 22:42:27 +0000 Subject: [PATCH 8/8] add stealth (no blueprint) definition option --- blueprint/src/chapter/reductions.tex | 2 +- blueprint/src/macro/common.tex | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/blueprint/src/chapter/reductions.tex b/blueprint/src/chapter/reductions.tex index df2e2011..56215e6c 100644 --- a/blueprint/src/chapter/reductions.tex +++ b/blueprint/src/chapter/reductions.tex @@ -66,7 +66,7 @@ \section{Galois representations and elliptic curves} \section{The Frey curve} \begin{stealthdefinition}[Frey] - Given a Frey package $(a,b,c,p)$, the corresponding \emph{Frey curve} (considered by Frey and, before him, Hellegouarch) is the elliptic curve $E$ defined by the equation $Y^2=X(X-a^p)(X+b^p)$\end{definition} + Given a Frey package $(a,b,c,p)$, the corresponding \emph{Frey curve} (considered by Frey and, before him, Hellegouarch) is the elliptic curve $E$ defined by the equation $Y^2=X(X-a^p)(X+b^p)$\end{stealthdefinition} \begin{theorem}\label{Frey_curve}\lean{FLT.FreyCurve} The Frey curve is an elliptic curve over $\Q$. diff --git a/blueprint/src/macro/common.tex b/blueprint/src/macro/common.tex index 5989f52f..31589358 100644 --- a/blueprint/src/macro/common.tex +++ b/blueprint/src/macro/common.tex @@ -7,3 +7,7 @@ \newcommand{\GQ}{\Gal(\Qbar/\Q)} \DeclareMathOperator{\Gal}{Gal} \DeclareMathOperator{\Aut}{Aut} +\usepackage{amsthm} + +\newtheorem{stealthdefinition}{Definition}[chapter] +