Merge branch 'main' of github.com:ImperialCollegeLondon/FLT

Author: kbuzzard

.gitignore

@@ -3,11 +3,14 @@
 /lake-packages/*
 .lake/*
 .DS_Store
+# Lean blueprint
 blueprint/print/print.log
 blueprint/web/
+blueprint/src/web.paux
+blueprint/src/web.bbl
 blueprint/print/
 # KB guesses this is safe (he's asked Patrick)
-blueprint/lean_decls
+blueprint/lean_decls 
 # Files generated by LaTeX
 *.aux
 *.bbl
@@ -18,4 +21,5 @@ blueprint/lean_decls
 *.fls
 *.fdb_latexmk
 *.synctex.gz
-
+# Python virtual environment 
+/.venv

blueprint/src/chapter/ch03frey.tex

@@ -410,6 +410,6 @@ \section{Hardly ramified representations}
 
 \begin{theorem}\label{Frey_curve_irreducible} The $\ell$-torsion in the Frey curve associated to a Frey package $(a,b,c,\ell)$ is irreducible.
 \end{theorem}
-\begin{proof}\uses{Frey_curve_reducible_structure, Frey_curve_no_trivial_submodule, Frey_curve_no_trivial_quotient,EllipticCurve.n_torsion_dimension} Follows from theorem~\ref{Frey_curve_reducible_structure}, corollary~\ref{Frey_curve_no_trivial_submodule}
+\begin{proof}\uses{Frey_curve_reducible_structure, Frey_curve_no_trivial_submodule, Frey_curve_no_trivial_quotient,Elliptic_curve_n_torsion_2d} Follows from theorem~\ref{Frey_curve_reducible_structure}, corollary~\ref{Frey_curve_no_trivial_submodule}
   and corollary~\ref{Frey_curve_no_trivial_quotient}.
 \end{proof}

blueprint/src/chapter/chtopbestiary.tex

@@ -66,7 +66,7 @@ \section{Results from class field theory}
 then let $\A_N^f:= N\otimes_{\Z}\widehat{\Z}$
 denote the finite adeles of $N$ and let $N_\infty := N\otimes_{\Q}\R$ denote the product of the completions of $N$ at the infinite places, so $\A_N:=\A_N^f\times N_\infty$ is the ring of adeles of $N$.
 
-\begin{theorem}\label{global_class_field_theory}\uses{local_class_field_theory}\notready If $N$ is a finite extension of $\Q$ then there are two ``canonical'' isomorphisms of topological groups between the profinite abelian groups $\pi_0(\A_N^\times/N^\times)$ and $\GN^{\ab}$; one sends local uniformisers to arithemtic Frobenii and the other to geometric Frobenii; each of the global isomorphisms is compatible with the local isomorphisms above.
+\begin{theorem}\label{global_class_field_theory}\uses{local_class_field_theory}\notready If $N$ is a finite extension of $\Q$ then there are two ``canonical'' isomorphisms of topological groups between the profinite abelian groups $\pi_0(\A_N^\times/N^\times)$ and $\GN^{\ab}$; one sends local uniformisers to arithmetic Frobenii and the other to geometric Frobenii; each of the global isomorphisms is compatible with the local isomorphisms above.
 \end{theorem}
 \begin{proof}\notready This is the main theorem of global class field theory; see for example Tate's article in~\cite{cf}.
 \end{proof}