diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index a413845..8e1f5c8 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -1,6 +1,6 @@ \title{Fermat's Last Theorem for regular primes} -\author{Demo Author} + \home{https://leanprover-community.github.io/flt-regular/} diff --git a/blueprint/src/demo.tex b/blueprint/src/demo.tex index 651efa4..c9be293 100644 --- a/blueprint/src/demo.tex +++ b/blueprint/src/demo.tex @@ -408,7 +408,7 @@ \section{Kummer's Lemma} Let $K$ be a number fields and $\a \in K$. Then there exists a $n \in \ZZ\backslash\{0\}$ such that $n \a$ is an algebraic integer. \end{lemma} -\begin{theorem}\label{Hilbert90} +\begin{theorem}[Hilbert 90]\label{Hilbert90} Let $K/F$ be a Galois extension of number fields whose Galois group $\Gal(K/F)$ is cyclic with generator $\sigma$. If $\a \in K$ is such that $N_{K/F}(\a)=1$, then \[ \a =\beta/ \sigma(\beta)\] for some $\beta \in \OO_K$. @@ -423,44 +423,73 @@ \section{Kummer's Lemma} \end{proof} -\begin{lemma}\label{lem:HilbertNot90} +\begin{theorem}[Hilbert 92]\label{lem:Hilbert92} Let $K/F$ be a Galois extension of $F=\QQ(\zeta_p)$ with Galois group $\Gal(K/F)$ cyclic with generator $\sigma$. Then there exists a unit $\eta \in \OO_K$ such that $N_{K/F}(\eta)=1$ but does not have the form $\epsilon/\sigma(\epsilon)$ for any unit $\e \in \OO_K$. -\end{lemma} +\end{theorem} \begin{proof} - Let \[U_1= \OO_K^\times / \OO_F^\times \qquad \text{and} \qquad U=U_1/U_{1,tors}.\] By Dirichlet's unit theorem we know $U$ is a free abelian group of rank $m=(p-1)^2/2$ generators\footnote{ Can we get away without knowing the exact rank?}. For any $f =\sum_n a_n x^n \in \ZZ[x]$ and $\a \in K$ we let $\a^f$ denote $\prod_n \sigma^n(\a)^{a_n}$. For any $\theta_i \in U$, let $S(\theta_1, \dots,\theta_r)$ denote the set of $\sigma^i(\theta_j)$ for $i \in \{0,\dots,p-2\}$ and $j \in \{1,\dots,r\}$. - - \paragraph{\textbf{Claim 1:}} There exist $\theta_1,\dots,\theta_m$ such that the elements of $S(\theta_1, \dots,\theta_m)$ are multiplicatively independent, therefore $S(\theta_1, \dots,\theta_m)$ generates a subgroup of finite index in $U$. - - - \paragraph{\textbf{Claim 2:}} If $\theta_i$ are chosen so that the index of $S(\theta_1, \dots,\theta_m)$ in $U$ is minimal, then no $\theta_i$ has the form $\theta^{1-\sigma}$ for $\theta \in U$. - +This is Hilbert theorem 92 (\cite{Hilbert}), also Lemma 33 of Swinnerton-Dyer's book (\cite{SD}). - \paragraph{\textbf{Claim 3:}} If $a_i \in \ZZ$ are not all divisible by $p$, then $\prod_i \theta_i^{a_i}$ is not of the form $\theta^{1-\sigma}$ for $\theta \in U$. - - Using these claims we can finish the proof as follows: We fist assume that $\zeta_p= \xi^{1-\sigma}$ with $\xi \in \OO_K^\times$ as otherwise we can take $\eta=\zeta_p$. By construction it follows that $\xi^p=N_{K/F}(\xi)$ is a unit in $F$ and $\xi$ is not in $F$. Picking representatives $\eta_i \in \OO_K^\times$ for the $\theta_i$ we can consider the group they generate, denoted $S(\eta_i)$. There is a map \[\phi: S(\eta_i) \to \OO_F^\times/\mu_F\] induced by $N_{K/F}$, where $\mu_F$ denote the $p$-th roots of unity in $F$. There are now three possibilities: - - - \begin{enumerate}[(a)] - \item $\xi^p$ is a primitive $p$-th root of unity. In this case we can pick $\eta$ as follows: +\end{proof} - \item No non-trivial power of $\xi^p$ is in the image of $\phi$ - \item Neither (a) or (b) hold. - \end{enumerate} - - +\section{Some Ramification results} + +We will need several results about ramification in degree $p$ extensions of $\QQ(\zeta_p)$. Following \cite{SD} we do this by using the relative different ideal of the extension. + +\begin{definition} + + Let $K, F$ be number fields with $F \subseteq K$. Let $A$ be an additive subgroup of $K$. Let \[A^{-1}=\{ \a \in K | \a A \in \OO_K\}\] and + \[A^* = \{ \a \in K | \Tr_{K/F} (\a A) \in \OO_F\}.\] The relative different $\frak{d}_{K/F}$ of $K/F$ is then defined as $((\OO_K)^*)^{-1}$ which one checks is an integral ideal in $\OO_K$. This is also the annihilator of $\Omega^1_{\OO_K/\OO_F}$ if we want to be fancy. +\end{definition} + + +\begin{lemma}\label{lem:diff_ideal_eqn} + Let $K/F$ be an extension of number fields and let $S$ denote the set of $\a \in \OO_K$ be such that $K=F(\a)$. Then \[ \gothd_{K/F} = \left (m_{\a}'(\a) : \a \in S \right )\] where $m_\a$ is denotes the minimal polynomial of $\a$. +\end{lemma} + +\begin{proof} + This is \cite[Theorem 20]{SD} \end{proof} +\begin{lemma}\label{lem:diff_ram} + Let $K/F$ be an extension of number fields with $\gothp_F, \gothp_K$ prime ideas in $K,F$ respectively, with $\gothp_K^e \parallel \gothp_F$ for $e >0$. Then $\gothp_K^{e-1} \mid \gothd_{K/F}$ and $\gothp_K^{e} \mid \gothd_{K/F}$ iff $\gothp_F \mid e$. +\end{lemma} + +\begin{proof} + \cite[Theorem 21]{SD} +\end{proof} + +\begin{lemma}\label{lem:loc_ramification} +Let $K$ be a number field, $p$ be a rational prime below $\gothp$ and let $\a_0, \xi$ be in $\OO_\gothp^\times$ (the units of the ring of integers of the completion of $K$ at $\gothp$) be such that \[\a_0^p \equiv \xi \mod \gothp^{m+r}\] where $\gothp^m \parallel p$ and $r(p-1)>m$. Then there exists an $\a \in \OO_{\gothp}^\times$ such that $\a^p =\xi$. + +\end{lemma} + +\begin{proof} + This is \cite[Lemma 20]{SD} +\end{proof} \begin{lemma}\label{lem:ramification_lem} +\uses{lem:loc_ramification,lem:diff_ideal_eqn,lem:diff_ram} Let $F=\QQ(\zeta_p)$ with $\zeta_p$ a primitive $p$-th root of unity. If $\xi \in \OO_F$ and coprime to $\lam_p:=1-\zeta_p$ and if \[\xi \equiv \a_0^p \mod \lam_p^p \] for some $\a_0 \in \OO_{F_\gothp}^\times$ (the ring of integers of the completion of $F$ at $\lam_p$), then the ideal $(\lam_p)$ is unramified in $K/F$ where $K=F(\sqrt[p]{\xi})$. \end{lemma} +\begin{proof} + Suppose that we have $\xi = \a_0^p \mod \lam_p^{p+1}$. The using \ref{lem:loc_ramification} with $m=p-1,r=2$ gives an $\a$ such that $\a^p=\xi$ in $\OO_{F_\gothp}^\times$. Meaning that $(\lam_p)$ is split in the local extension and hence split in $K/F$ (note: add this lemma explictly somewhere). + + If we instead have $\lam_p^p \parallel (\xi-\a_0^p)$, then pick some element in $ K$ which agrees with $\a_0$ up to $\lam_p^{p+1}$, which we again call $\a_0$ and consider \[\eta= (\sqrt[p]{\xi}-\a_0)/\lam_p\] so that $K=F(\eta)$. Now, if $m_\eta$ is the minimal monic polynomial for $\eta$ then by definition it follows that \[m_\eta(x) \equiv x^p+\left (\a_0^{p-1}p/\lam_p^{p-1} \right )x+ (\a_0^p-\xi)/\lam_p^p \mod \lam_p\] + + So in fact $\eta \in \OO_K$. Now, if we look at $m_\eta'$ we see that $m_\eta'(\eta)$ is coprime to $\lam_p$ and therefore coprime to $\gothd_{K/F}$ (by \ref{lem:diff_ideal_eqn}) and therefore $\lam_p$ is unramified (by \ref{lem:diff_ram}). + +\end{proof} + + + +\section{Proof of Kummers Lemma} +Using the above we have the following lemma (from which Kummer's lemma is immediate): -Before giving the proofs of the above, we will first show how one can use this to prove the following lemma (from which Kummer's lemma is immediate): \begin{lemma}\label{Kummer_alt} Let $u \in F$ with $F=\QQ(\zeta_p)$ be a unit such that \[u \equiv a^p \mod \lam_p^p\] for some $a \in \OO_F$. The either $u = \epsilon^p$ for some $\epsilon \in \OO_F^\times$ or $p$ divides the class number of $F$. @@ -468,12 +497,10 @@ \section{Kummer's Lemma} \end{lemma} \begin{proof} - Assume $u$ is not a $p$-th power. Then let $K=F(\sqrt[p]{u})$ and $\eta \in K$ be as in \ref{lem:HilbertNot90}. Then $K/F$ is Galois and cyclic of degree $p$. Not by Hilbert 90 (\ref{Hilbert90}) we can find $\beta \in \OO_K$ such that \[\eta = \beta/\sigma(\beta)\] (but note that by our assumption $\beta$ is not a unit). Note that the ideal $(\eta)$ is invariant under $\Gal(K/F)$ by construction and by \ref{lem:ramification_lem} it cannot be ramified, therefore $(\beta)$ is the extension of scalars of some ideal $\gothb$ in $\OO_F$. Now if $\gothb$ is principal generated by some $\gamma$ then $\beta=v \gamma$ for some $v \in \OO_K^\times$. But this means that \[\eta = \beta/\sigma(\beta)= v/(\sigma(v)) \cdot \gamma / \sigma(\gamma)=v/\sigma(v) \] contradicting our assumption coming from \ref{lem:HilbertNot90}. On the other hand, $\gothb^p= N_{K/F}(\beta)$ is principal, meaning $p$ divides the class group of $F$. - - - - + Assume $u$ is not a $p$-th power. Then let $K=F(\sqrt[p]{u})$ and $\eta \in K$ be as in \ref{lem:Hilbert92}. Then $K/F$ is Galois and cyclic of degree $p$. Now by Hilbert 90 (\ref{Hilbert90}) we can find $\beta \in \OO_K$ such that \[\eta = \beta/\sigma(\beta)\] (but note that by our assumption $\beta$ is not a unit). Note that the ideal $(\eta)$ is invariant under $\Gal(K/F)$ by construction and by \ref{lem:ramification_lem} it cannot be ramified, therefore $(\beta)$ is the extension of scalars of some ideal $\gothb$ in $\OO_F$. Now if $\gothb$ is principal generated by some $\gamma$ then $\beta=v \gamma$ for some $v \in \OO_K^\times$. + But this means that \[\eta = \beta/\sigma(\beta)= v/(\sigma(v)) \cdot \gamma / \sigma(\gamma)=v/\sigma(v) \] contradicting our assumption coming from \ref{lem:Hilbert92}. On the other hand, $\gothb^p= N_{K/F}(\beta)$ is principal, meaning $p$ divides the class group of $F$ as required. \end{proof} + diff --git a/blueprint/src/references.bib b/blueprint/src/references.bib index d29ad46..ce9771f 100644 --- a/blueprint/src/references.bib +++ b/blueprint/src/references.bib @@ -84,4 +84,13 @@ @book {SD year={2001}, collection={London Mathematical Society Student Texts} } - \ No newline at end of file + +@book{Hilbert, + title={The Theory of Algebraic Number Fields}, + author={Hilbert, D. and Lemmermeyer, F. and Adamson, I.T. and Schappacher, N. and Schoof, R.}, + isbn={9783540627791}, + lccn={98042185}, + url={https://books.google.co.uk/books?id=_Q2h83Bm94cC}, + year={1998}, + publisher={Springer Berlin Heidelberg} +} \ No newline at end of file