diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index 7d65fbd2..12429f6b 100644 --- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean +++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean @@ -1,4 +1,7 @@ -import Mathlib -- **TODO** fix when finished or if `exact?` is too slow +--import Mathlib -- **TODO** fix when finished or if `exact?` is too slow +import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing +import Mathlib.NumberTheory.NumberField.Basic +import Mathlib.NumberTheory.RamificationInertia /-! # Base change of adele rings. @@ -6,8 +9,9 @@ import Mathlib -- **TODO** fix when finished or if `exact?` is too slow If `A` is a Dedekind domain with field of fractions `K`, if `L/K` is a finite separable extension and if `B` is the integral closure of `A` in `L`, then `B` is also a Dedekind domain. Hence the rings of finite adeles `𝔸_K^∞` and `𝔸_L^∞` (defined using `A` and `B`) -are defined, and there's a canonical map `L βŠ—[K] 𝔸_K^∞ β†’ 𝔸_L^∞`. The main theorem -of this file is that it's an isomorphism. This result should be in mathlib. +are defined. In this file we define the natural `K`-algebra map `𝔸_K^∞ β†’ 𝔸_L^∞` and +the natural `L`-algebra map `𝔸_K^∞ βŠ—[K] L β†’ 𝔸_L^∞`, and show that the latter map +is an isomorphism. -/ @@ -34,11 +38,10 @@ variable [Algebra.IsIntegral A B] -- I can't find in mathlib the assertion that B is a finite A-moduie. -- It should follow from L/K finite. +example : Module.Finite A B := by sorry -- I assume this is correct /- -Conjecture: in this generality there's a natural isomorphism `L βŠ—[K] 𝔸_K^∞ β†’ 𝔸_L^∞` -I've not found a reference for this but we can try following the usual -references (which work for global fields). This is what we do below. +In this generality there's a natural isomorphism `L βŠ—[K] 𝔸_K^∞ β†’ 𝔸_L^∞` . Update: Javier suggests p21 of https://math.berkeley.edu/~ltomczak/notes/Mich2022/LF_Notes.pdf @@ -56,30 +59,19 @@ def comap (w : HeightOneSpectrum B) : HeightOneSpectrum A where isPrime := Ideal.comap_isPrime (algebraMap A B) w.asIdeal ne_bot := mt Ideal.eq_bot_of_comap_eq_bot w.ne_bot --- lemma: pushforward of pullback is P^(ram index) -lemma map_comap (w : HeightOneSpectrum B) : - (w.comap A).asIdeal.map (algebraMap A B) = - w.asIdeal ^ ((Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal)) := by - -- This must be standard? Maybe a hole in the library for Dedekind domains - -- or maybe I just missed it? - sorry - open scoped algebraMap - - -- Need to know how the valuation `w` and its pullback are related on elements of `K`. -def valuation_comap (w : HeightOneSpectrum B) (x : K) : +lemma valuation_comap (w : HeightOneSpectrum B) (x : K) : (comap A w).valuation x = w.valuation (algebraMap K L x) ^ (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) := by - -- This should follow from map_comap? sorry -- Say w is a finite place of L lying above v a finite places -- of K. Then there's a ring hom K_v -> L_w. variable {B L} in -noncomputable def adicCompletion_comap (w : HeightOneSpectrum B) : +noncomputable def adicCompletion_comap_ringHom (w : HeightOneSpectrum B) : (adicCompletion K (comap A w)) β†’+* (adicCompletion L w) := letI : UniformSpace K := (comap A w).adicValued.toUniformSpace; letI : UniformSpace L := w.adicValued.toUniformSpace; @@ -106,12 +98,12 @@ noncomputable local instance (w : HeightOneSpectrum B) : (algebraMap L (adicCompletion L w)).comp (algebraMap K L) variable {B L} in -noncomputable def adicCompletion_alg_comap (w : HeightOneSpectrum B) : +noncomputable def adicCompletion_comap_algHom (w : HeightOneSpectrum B) : letI : Algebra K (adicCompletion L w) := RingHom.toAlgebra <| (algebraMap L (adicCompletion L w)).comp (algebraMap K L); letI : Module K (adicCompletion L w) := Algebra.toModule (HeightOneSpectrum.adicCompletion K (comap A w)) β†’β‚—[K] (HeightOneSpectrum.adicCompletion L w) := - sorry -- use `adicCompletion_comap` and prove it's a K-algebra homomorphism + sorry -- use `adicCompletion_comap_ringHom` and prove it's a K-algebra homomorphism end IsDedekindDomain.HeightOneSpectrum @@ -126,11 +118,11 @@ open scoped TensorProduct -- βŠ— notation for tensor product noncomputable local instance : Algebra K (ProdAdicCompletions B L) := RingHom.toAlgebra <| (algebraMap L (ProdAdicCompletions B L)).comp (algebraMap K L) --- These should be easy +-- These should be easy but I've just noticed that it should be an alghom noncomputable def ProdAdicCompletions.baseChange : L βŠ—[K] ProdAdicCompletions A K β†’β‚—[K] ProdAdicCompletions B L := TensorProduct.lift <| { toFun := fun l ↦ { - toFun := fun kv w ↦ l β€’ (adicCompletion_comap A K w (kv (comap A w))) + toFun := fun kv w ↦ l β€’ (adicCompletion_comap_algHom A K w (kv (comap A w))) map_add' := sorry map_smul' := sorry } diff --git a/blueprint/lean_decls b/blueprint/lean_decls index fdd6bfdc..ad4dc4e5 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -76,12 +76,14 @@ Bourbaki52222.f_exists Bourbaki52222.algebraic Bourbaki52222.normal Bourbaki52222.separableClosure_finrank_le +NumberField.AdeleRing.discrete +NumberField.AdeleRing.cocompact +NumberField.AdeleRing.locallyCompactSpace +IsDedekindDomain.HeightOneSpectrum.valuation_comap +IsDedekindDomain.HeightOneSpectrum.adicCompletion_comap_algHom +DedekindDomain.ProdAdicCompletions.baseChange TotallyDefiniteQuaternionAlgebra.AutomorphicForm TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup TotallyDefiniteQuaternionAlgebra.AutomorphicForm.module TotallyDefiniteQuaternionAlgebra.AutomorphicForm.finiteDimensional -DivisionAlgebra.finiteDoubleCoset -NumberField.AdeleRing.discrete -NumberField.AdeleRing.cocompact -NumberField.AdeleRing.locallyCompactSpace -IsDedekindDomain.HeightOneSpectrum.adicCompletion_alg_comap \ No newline at end of file +DivisionAlgebra.finiteDoubleCoset \ No newline at end of file diff --git a/blueprint/src/chapter/AdeleMiniproject.tex b/blueprint/src/chapter/AdeleMiniproject.tex new file mode 100644 index 00000000..19d31e60 --- /dev/null +++ b/blueprint/src/chapter/AdeleMiniproject.tex @@ -0,0 +1,168 @@ +\chapter{Miniproject: Adeles}\label{Adele_miniproject} + +\section{Status} + +This is an active miniproject. + +\section{The goal} + +At the time of writing, mathlib does not have a definition of the adeles of +a number field. There are several goals to this miniproject. + +\begin{itemize} + \item Define the adeles $\A_K$ of a number field~$K$ and + give them the structure of a $K$-algebra; + \item Prove that $\A_K$ is a locally compact topological ring; + \item Show that if $L/K$ is a finite extension of number fields then the + natural map $L\otimes_K\A_K\to\A_L$ is an isomorphism; + \item Prove that $K \subseteq \A_K$ is a discrete subgoup and the quotient is compact. +\end{itemize} + +We briefly go through the basic definitions. A cheap definition of the finite +adeles $\A_K^\infty$ of $K$ is $K\otimes_{\Z}\Zhat$, where $\Zhat$ is +the profinite completion of the integers. A cheap definition of the infinite adeles +$K_\infty$ of $K$ is $K\otimes_{\Q}\R$, and a cheap definition of the adeles +of $K$ is $\A_K^\infty\times K_\infty$. However in the literature different definitions +are often given. The finite adeles of $K$ are usually defined +as the so-called restricted product $\prod'_{\mathfrak{p}}K_{\mathfrak{p}}$ over the completions +$K_{\mathfrak{p}}$ of $K$ at all maximal ideals $\mathfrak{p}\subseteq\mathcal{O}_K$ of the +integers of $K$. Here the restricted product is the subset of $\prod_{\mathfrak{p}}K_{\mathfrak{p}}$ +consisting of elements which are in $\mathcal{O}_{K,\mathfrak{p}}$ for all but finitely many +$\mathfrak{p}$. +Mathlib already has the finite adeles and the proof that they're a topological ring; +in fact the construction in mathlib works for any Dedekind domain. + +Similarly the infinite adeles of a number field +are usually defined as $\prod_v K_v$, +the product running over the archimedean completions of~$K$. + +\section{Current status} + +Salvatore Mercuri has made great progress with the definition of $\A_K$ and he even +has a complete formalisation of the proof that the adele ring is locally compact. His work is in +\href{https://github.com/smmercuri/adele-ring_locally-compact}{his own repo} which +I don't want to have as a dependency of FLT, because this work should all be +in mathlib. We quote some of it here. + +\section{Results about adeles of a number field that we await} + +Let $K$ be a number field. Right now mathlib has the finite adeles $\A_K^\infty$ of $K$, +with its topological ring structure. It does not however have the infinite adeles $K_\infty$. +There are PRs by Salvatore Mercuri currently +in progress for defining this topological ring. Once we have it, the full ring of +adeles $\A_K$ is defined as $\A_K:=\A_K^\infty\times K_\infty$; it is a topological ring +and also a $K$-algebra. Once Mercuri's mathlib +PR~\href{https://github.com/leanprover-community/mathlib4/pull/16485}{16485} is merged, we will have +all this available to us; until then, we sorry the definitions and these facts. + +Mercuri's work isn't however enough for us; we also need several theorems about this topological +$K$-algebra. These lemmas are essentially impossible to work on until we have the definition in +mathlib. We state them here without proof. + +\begin{theorem} + \lean{NumberField.AdeleRing.discrete} + \label{NumberField.AdeleRing.discrete} + The additive subgroup $K$ of $\A_K$ is discrete. +\end{theorem} + +\begin{theorem} + \lean{NumberField.AdeleRing.cocompact} + \label{NumberField.AdeleRing.cocompact} + The quotient $\A_K/K$ is compact. +\end{theorem} + +\begin{theorem} + \lean{NumberField.AdeleRing.locallyCompactSpace} + \label{NumberField.AdeleRing.locallyCompact} + The topological ring $\A_K$ is locally compact. +\end{theorem} + +Mercuri has already proved local compactness in his repo. +As far as I know, the other +two theorems remain unformalised (but as I've mentioned, we cannot start on them until +we have a definition of the adele ring in this project, and I would prefer +that this were achieved by upstreaming Mercuri's work to mathlib). + +However, there is something that we can do here even before Mercuri's work +is upstreamed: one proof I know that of discreteness +and cocompactness of $K$ in $\A_K$ reduces to the case $K=\Q$, using the ``canonical'' +isomorphism $\A_K\cong\A_{\Q}\otimes_{\Q}K$. This can be proved by checking it for finite +and infinite adeles separately, so one thing which we can work on now is the finite case. +We explain this in the next section. + +\section{Results about finite adeles which we can work on now} + +Adeles are arithmetic objects, attached to global fields like number fields. +However (as I learnt from Maria Ines de Frutos Fernandez) finite adeles are algebraic +objects, as they can be attached to any Dedekind domain. The ``theorem'' that we need +is the following: + +\begin{theorem} + Let~$A$ be a Dedekind domain with field of fractions~$K$, and write $\mathbb{A}_{A,K}^\infty$ + for the finite adeles of $A$. Let~$L/K$ be a finite + separable extension, and let $B$ be the integral closure of~$A$ in~$L$. + Then there's a ``canonical'' isomorphism $\mathbb{A}_{R,K}^\infty \otimes_KL\mathbb{A}_{B,L}^\infty$. +\end{theorem} + +Of course, this isn't a theorem; this is actually a \emph{definition} (the map) and a theorem about +the definition (that it's an isomorphism). Before we can prove the theorem, we need to make the +definition. + +If $A$ is a Dedekind domain then the \emph{height one spectrum} of $A$ is +the nonzero prime ideals of~$A$. Note that because we stick to the literature, +rather than to common sense, fields are Dedekind domains in mathlib, and the +height one spectrum of a field is empty. The reason I don't like allowing fields +to be Dedekind domain is that geometrically the standard definition of Dedekind +domain is ``smooth affine curve, or a point''. But many theorems in algebraic geometry +begin ``let $C$ be a smooth curve''. + +There are two steps to the definition of the map; the first is to define it locally +on the individual completions and the second is to glue everything together. Let's +start with the local construction. + +Say we're in the AKLB setup above, with $L/K$ a finite separable extension. +Let $w$ be a finite place of $L$ lying above a finite place $v$ of $K$. +We put the $w$-adic topology on $L$ and the $v$-adic topology on~$K$. We now claim +that inclusion $i:K\to L$ is continuous with respect to these topologies. This +claim follows from + +\begin{lemma} If $i:K\to L$ denotes the inclusion then $e*w(i(k))=v(k)$, where + $e$ is the ramification index of $w/v$. + \label{IsDedekindDomain.HeightOneSpectrum.valuation_comap} + \lean{IsDedekindDomain.HeightOneSpectrum.valuation_comap} +\end{lemma} +\begin{proof} + Standard. +\end{proof} + +\begin{definition} + \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletion_comap_algHom} + \label{IsDedekindDomain.HeightOneSpectrum.adicCompletion_comap_algHom} + \uses{IsDedekindDomain.HeightOneSpectrum.valuation_comap} + There's a natural continuous $K$-algebra homomorphism map $K_v\to L_w$. It is defined by completing + the inclusion $K\to L$ at the finite places $v$ and $w$, which can be done + by the previous lemma. +\end{definition} + +Note: the formalization right now only claims that the map is a $K$-algebra homomorphism, +not the continuity. Do we have continuous $K$-algebra maps? + +We can take the product of all of these maps. + +\begin{definition} + \lean{DedekindDomain.ProdAdicCompletions.baseChange} + \label{DedekindDomain.ProdAdicCompletions.baseChange} + \uses{IsDedekindDomain.HeightOneSpectrum.adicCompletion_comap_algHom} + There's a natural $K$-algebra homomorphism $\prod_v K_v\to\prod_w L_w$, where the + products run over the height one spectrums of $A$ and $B$ respectively. +\end{definition} + +One then has to check that for good primes everything works on an integral level, + +\begin{definition} + The map above induces a natural $K$-algebra homomorphism $\A_K^\infty\to\A_L^\infty$ + at the level of finite adeles. +\end{definition} + +Note that the finite adeles do not have the subspace topology, so one has to be slightly +careful here. diff --git a/blueprint/src/chapter/QuaternionAlgebraProject.tex b/blueprint/src/chapter/QuaternionAlgebraProject.tex index a84b250f..45f4fb0e 100644 --- a/blueprint/src/chapter/QuaternionAlgebraProject.tex +++ b/blueprint/src/chapter/QuaternionAlgebraProject.tex @@ -37,7 +37,7 @@ \section{Initial definitions} this fact in ongoing project work. A \emph{totally real field} is a number field~$F$ such that the image of every ring -homomorphism $F\to\bbC$ is a subset of $\R$. We fix a totally real field~$F$ and a +homomorphism $F\to\bbC$ is a subset of $\R$. We fix once and for all a totally real field~$F$ and a quaternion algebra $D$ over $F$. We furthermore assume that $D$ is \emph{totally definite}, that is, that for all field embeddings $\tau:F\to\R$ we have $D\otimes_{F,\tau}\R\cong\bbH$. @@ -59,17 +59,10 @@ \section{The adelic viewpoint} Having made assumptions on $D$ which makes the theory far less technical, we will now make it a little more technical by using the modern adelic approach to the theory. -In particular, we need to bring in the finite adeles of $F$. This is a huge topological ring -denoted $\A_F^\infty$, which has a cheap definition as $F\otimes_{\Z}\Zhat$, where $\Zhat$ is -the profinite completion of the integers, but which is often explained in the literature -as the restricted product $\prod'_{\mathfrak{p}}F_{\mathfrak{p}}$ over the completions -$F_{\mathfrak{p}}$ of $F$ at all maximal ideals $\mathfrak{p}\subseteq\mathcal{O}_F$ of the -integers of $F$. The restricted product is the subset of $\prod_{\mathfrak{p}}F_{\mathfrak{p}}$ -consisting of elements which are in $\mathcal{O}_{F,\mathfrak{p}}$ for all but finitely many -$\mathfrak{p}$. -Mathlib already has the finite adeles and the proof that they're a topological ring. If you are -not familiar with this kind of object, just remember that it is a commutative -$F$-algebra $\A_F^\infty$ with a topology, because this is all we shall need for now. +The adeles of a number field are discussed in far more detail +in the adele miniproject \ref{Adele_miniproject}. We just recall here that if $K$ is a number field +then there are two huge topological $K$-algebras called the \emph{finite adeles} +$\A_K^\infty$ and the \emph{adeles} $\A_K$ of $K$. Let us now fix a \emph{weight}, a \emph{level} and a \emph{character}, and we will define a space of automorphic forms for $D^\times$ of this weight, level and character. If you know @@ -80,8 +73,9 @@ \section{The adelic viewpoint} A \emph{weight} is a finitely-generated $R$-module~$W$ with an action of $D^\times$. For applications to Fermat's Last Theorem we only need to consider the case where $W=R$ and the action is trivial, -but there is no harm in setting things up in more generality. The case $W=R$ corresponds (via -the highly non-trivial Jacquet-Langlands correspondence) to the case of modular forms of weight 2. +but there is no harm in setting things up in more generality. The case $W=R=\bbC$ corresponds (via +the highly non-trivial Jacquet-Langlands correspondence) when $F=\Q$ to the case of modular forms +of weight 2, and for general~$F$ corresponds to Hilbert modular forms of parallel weight~2. A \emph{level} is a compact open subgroup~$U$ of $(D\otimes_F\A_F^\infty)^\times$. These are plentiful. The ring $D\otimes_F\A_F^\infty$ is a topological ring, and this fact is currently in the process @@ -200,93 +194,9 @@ \section{Statement of the main result of the miniproject} and because $f_1(g_i)=f_2(g_i)$ by assumption, we deduce $f_1(g)=f_2(g)$ as required. \end{proof} -It thus remains to prove Fujisaki's lemma. +It thus remains to prove Fujisaki's lemma. Note that we will be assuming the results +from the adele mini-project~\ref{Adele_miniproject}. -\section{Results about adeles of a number field that we await} +\section{Proof of Fujisaki's lemma} -Let $K$ be a number field. Right now mathlib has the finite adeles $\A_K^\infty$ of $K$, -with its topological ring structure. It does not however have the infinite adeles $K_\infty$, -which can be defined either as $K\otimes_{\Q}\R$ or as $\prod_{v\infty}K_v$, where -$v$ runs through the infinite places of $K$. There are PRs by Salvatore Mercuri currently -in progress for defining this topological ring. Once we have it, the full ring of -adeles $\A_K$ is defined as $\A_K:=\A_K^\infty\times K_\infty$; it is a topological ring -and also a $K$-algebra. Once Mercuri's mathlib PR `16485` is merged, we will have -all this available to us; until then, we sorry the definitions and these facts. - -Mercuri's work isn't however enough for us; we also need several theorems about this topological -$K$-algebra. These lemmas are essentially impossible to work on until we have the definition in -mathlib. We state them here without proof. - -\begin{theorem} - \lean{NumberField.AdeleRing.discrete} - \label{NumberField.AdeleRing.discrete} - The additive subgroup $K$ of $\A_K$ is discrete. -\end{theorem} - -\begin{theorem} - \lean{NumberField.AdeleRing.cocompact} - \label{NumberField.AdeleRing.cocompact} - The quotient $\A_K/K$ is compact. -\end{theorem} - -\begin{theorem} - \lean{NumberField.AdeleRing.locallyCompactSpace} - \label{NumberField.AdeleRing.locallyCompact} - The topological ring $\A_K$ is locally compact. -\end{theorem} - -Mercuri has already proved local compactness in -\href{https://github.com/smmercuri/adele-ring_locally-compact}{his own repo} but rather than -depending on this repo, we should aim to have this in mathlib. As far as I know, the other -two theorems remain unformalised (but as I've mentioned, we cannot start on them until -we have a definition of the adele ring). - -However, there is something that we can do here: one proof I know that of discreteness -and cocompactness of $K$ in $\A_K$ reduces to the case $K=\Q$, using the ``canonical'' -isomorphism $\A_K\cong\A_{\Q}\otimes_{\Q}K$. This can be proved by checking it for finite -and infinite adeles separately, so one thing which we can work on now is the finite case. -We explain this in the next section. - -\section{Results about finite adeles which we can work on now} - -Adeles are arithmetic objects, attached to global fields like number fields. -However (as I learnt from Maria Ines de Frutos Fernandez) finite adeles are algebraic -objects, as they can be attached to any Dedekind domain. The ``theorem'' that we need -is the following: - -\begin{theorem} - Let~$A$ be a Dedekind domain with field of fractions~$K$, and write $\mathbb{A}_{A,K}^\infty$ - for the finite adeles of $A$. Let~$L/K$ be a finite - separable extension, and let $B$ be the integral closure of~$A$ in~$L$. - Then there's a ``canonical'' isomorphism $\mathbb{A}_{R,K}^\infty \otimes_KL\mathbb{A}_{B,L}^\infty$. -\end{theorem} - -Of course, this isn't a theorem; this is actually a \emph{definition} (the map) and a theorem about -the definition. Before we can prove the theorem, we need to make the definition. - -If $A$ is a Dedekind domain then the \emph{height one spectrum} of $A$ is -the nonzero prime ideals of~$A$. Note that because we stick to the literature, -rather than to common sense, fields are Dedekind domains in mathlib, and the -height one spectrum of a field is empty. - -There are two steps to the definition of the map; the first is to define it locally -on the individual completions and the second is to glue everything together. Let's -start with the local construction. I am not really clear about the generality in which one -wants this. Cassels' article in Cassels--Froehlich works with a general field equipped with -a real-valued norm, but we only need norms coming from points in the height one spectrum -on an AKLB setup, and also the cases of $\mathbb{R}$ and $\mathbb{C}$. - -So say we're in the AKLB setup, with $L/K$ a finite separable extension. -Let $w$ be a finite place of $L$ lying above a finite place $v$ of $K$. - -\begin{definition} - \lean{IsDedekindDomain.HeightOneSpectrum.adicCompletion_alg_comap} - \label{IsDedekindDomain.HeightOneSpectrum.adicCompletion_alg_comap} - There's a natural $K$-algebra homomorphism map $K_v\to L_w$. -\end{definition} - -This gives us a map $\prod_v K_v\to\prod_w L_w$ -and hence $L\otimes_K\prod_v K_v\to\prod_w L_w$ which presumably is an isomorphism. -One then has to check that for good primes everything works on an integral level, -thus giving the isomorphism on the finite adeles. One also has to check that it's a -topological isomorphism. +See Main Theorem 27.6.14 of Voight. TODO: make these into issues. diff --git a/blueprint/src/chapter/ch01introduction.tex b/blueprint/src/chapter/ch01introduction.tex index 20aa480c..c27072dc 100644 --- a/blueprint/src/chapter/ch01introduction.tex +++ b/blueprint/src/chapter/ch01introduction.tex @@ -1,9 +1,79 @@ \chapter{Introduction} -Fermat's Last Theorem is the statement that if $a,b,c,n$ are positive whole numbers with $n\geq 3$, then $a^n+b^n\not=c^n$. It is thus a statement about a family of \emph{Diophantine equations} ($a^3+b^3=c^3, a^4+b^4=c^4,\ldots$). Diophantus was a Greek mathematician who lived around 1800 years ago, and he would have been able to understand the statement of the theorem (he knew about positive integers, addition and multiplication). +Fermat's Last Theorem is the statement that if $a,b,c,n$ are positive whole numbers with $n\geq 3$, +then $a^n+b^n\not=c^n$. It is thus a statement about a family of \emph{Diophantine equations} +($a^3+b^3=c^3, a^4+b^4=c^4,\ldots$). Diophantus was a Greek mathematician who lived around 1800 +years ago, and he would have been able to understand the statement of the theorem (he knew about +positive integers, addition and multiplication). -Fermat's Last Theorem was explicitly raised by Fermat in 1637, and was proved by Wiles (with the proof completed in joint work with Taylor) in 1994. There are now several proofs but all of them go broadly in the same direction, using elliptic curves and modular forms. +Fermat's Last Theorem was explicitly raised by Fermat in 1637, and was proved by Wiles (with the +proof completed in joint work with Taylor) in 1994. There are now several proofs but all of them +go broadly in the same direction, using elliptic curves and modular forms. -Explaining a proof of Fermat's Last Theorem to Lean is in some sense like explaining the proof to Diophantus; for example, the proof starts by observing that before we go any further it's convenient to first invent/discover zero and negative numbers, and one can point explicitly at places in Lean's source code \href{https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Prelude.lean#L1049}{here} and \href{https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Data/Int/Basic.lean#L45}{here} where these things happen. However we will adopt a more efficient approach: we will assume all of the theorems both in Lean and in its mathematics library \href{https://github.com/leanprover-community/mathlib4}{\tt mathlib}, and proceed from there. To give some idea of what this entails: {\tt mathlib} at the time of writing contains most of an undergraduate mathematics degree and parts of several relevant Masters level courses (for example, the definitions and basic properties of \href{https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.html}{elliptic curves} and \href{https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/ModularForms/Basic.html}{modular forms} are in {\tt mathlib}). Thus our task can be likened to teaching a graduate level course on Fermat's Last Theorem to a computer. +Explaining a proof of Fermat's Last Theorem to Lean is in some sense like explaining the proof to +Diophantus; for example, the proof starts by observing that before we go any further it's convenient +to first invent/discover zero and negative numbers, and one can point explicitly at places in Lean's +source code \href{https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Prelude.lean#L1049}{here} +and \href{https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Data/Int/Basic.lean#L45}{here} +where these things happen. However we will adopt a more efficient approach: we will assume all of +the theorems both in Lean and in its mathematics library +\href{https://github.com/leanprover-community/mathlib4}{\tt mathlib}, and proceed from there. +To give some idea of what this entails: {\tt mathlib} at the time of writing contains most of an +undergraduate mathematics degree and parts of several relevant Masters level courses (for example, +the definitions and basic properties of +\href{https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.html}{elliptic curves} +and \href{https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/ModularForms/Basic.html}{modular forms} +are in {\tt mathlib}). Thus our task can be likened to teaching a graduate level course on +Fermat's Last Theorem to a computer. -The proof explained in these notes was constructed by Taylor, taking into account Buzzard's comments on what would be easy or hard to do in Lean. The proof uses refinements of the original Taylor-Wiles method by Diamond/Fujiwara, Khare-Wintenberger, Skinner-Wiles, Kisin, Taylor and others -- one could call it a 21st century proof of the theorem. We shall explain more about the exact path we're taking in Chapter~\ref{ch_overview}. But before we go into those technical details, we can enjoy some of the more basic arguments at the start of the proof. And the proof starts, as every known proof does, with some basic reductions and the introduction of a certain elliptic curve. We explain this in the next chapter. +\section{Which proof is being formalised?} + +At the time of writing, these notes do not contain anywhere near a proof of FLT, or even a sketch proof. +Over the next few years, we will be building parts of the argument, following a strategy +constructed by Taylor, taking into account Buzzard's comments on what would be easy or hard to do +in Lean. The proof uses refinements of the original Taylor-Wiles method by Diamond/Fujiwara, +Khare-Wintenberger, Skinner-Wiles, Kisin, Taylor and others -- one could call it a 21st century +proof of the theorem. We shall furthermore be assuming many nontrivial theorems without proof, +at least initially. For example we shall be assuming the existence of Galois representations +attached to weight~2 Hilbert modular forms, Langlands' cyclic base change theorem for $\GL_2$, +Mazur's theorem bounding the torsion subgroup of an elliptic curve over the rationals, and +several other nontrivial results which were known by the end of the 1980s. The first main goal +of the project is to state, and then prove, a modularity lifting theorem; the proof of such a theorem +was the key breakthrough introduced in Wiles' 1994 paper which historically completed the proof +of FLT. We will not be proving the original Wiles--Taylor-Wiles modularity lifting theorem, but +instead will prove a more general result which works for Hilbert modular forms. + +We shall say more about the exact path we're taking in +Chapter~\ref{ch_overview}. + +\section{The structure of this blueprint} + +The following chapter of the blueprint, chapter~\ref{ch_reductions}, explains how to reduce FLT +to two highly nontrivial statements about the $p$-torsion in a certain elliptic curve (the Frey curve). +It mostly comprises of some basic reductions and the introduction of the Frey curve. + +The chapter after that, chapter~\ref{ch_frey}, goes into more details about elliptic curves, +however we need so much material here that somehow the top-down approach felt quite overwhelming +at this point. For example even the basic claim that the $p$-torsion in the Frey curve curve is +a 2-dimensional mod $p$ Galois representation feels like quite a battle to formalise, +and proving that it is semistable and unramified outside $2p$ is even harder. +Several people are working on the basic theory of elliptic curves, and hopefully +we will be able to make more progess on this "top-down" approach later. + +The next chapter, chapter~\ref{ch_overview}, is an \emph{extremely} sketchy overview of how +the rest of the proof goes. There is so much to do here that I felt that there was little +point continuing with this; definition after definition is missing. + +All of the remaining chapters are experiments, and most of them are what I am currently +calling ``mini-projects''. A mini-project is a bottom-up project, typically at early graduate +student level, with a concrete goal. The ultimate goal of many of these projects is to actually +get some result into mathlib. We have had one success so far -- the Frobenius mini-project +is currently being PRed to mathlib by Thomas Browning. Currently most of my efforts are +going into running mini-projects, with the two most active ones currently being the adeles +mini-project and the quaternion algebra mini-project. These projects do not logically depend +on each other for the most part, and one can pick and choose how one reads them. + +We finish with an appendix, which is again very sketchy, and comprises mostly of a big +list of nontrivial theorems many of which we will be assuming without proof in the FLT +project, or at least not prioritising until we have proved the modularity lifing +theorem assuming them. diff --git a/blueprint/src/chapter/ch02reductions.tex b/blueprint/src/chapter/ch02reductions.tex index 519f3812..7956b4aa 100644 --- a/blueprint/src/chapter/ch02reductions.tex +++ b/blueprint/src/chapter/ch02reductions.tex @@ -1,4 +1,4 @@ -\chapter{First reductions of the problem} +\chapter{First reductions of the problem}\label{ch_reductions} \section{Overview} The proof of Fermat's Last Theorem is by contradiction. We assume that we have a counterexample $a^n+b^n=c^n$, and manipulate it until it satisfies the axioms of a ``Frey package''. From the Frey package we build a Frey curve -- an elliptic curve defined over the rationals. We then look at a certain representation of a Galois group coming from this elliptic curve, and finally using two very deep and independent theorems (one due to Mazur, the other due to Wiles) we show that this representation is neither reducible or irreducible, a contradiction. diff --git a/blueprint/src/chapter/ch03frey.tex b/blueprint/src/chapter/ch03frey.tex index b5401725..7cdbe5ed 100644 --- a/blueprint/src/chapter/ch03frey.tex +++ b/blueprint/src/chapter/ch03frey.tex @@ -1,4 +1,4 @@ -\chapter{Elliptic curves, and the Frey Curve} +\chapter{Elliptic curves, and the Frey Curve}\label{ch_frey} \section{Overview} @@ -12,7 +12,7 @@ \section{The arithmetic of elliptic curves} \begin{theorem}\label{EllipticCurve.n_torsion_card}\lean{EllipticCurve.n_torsion_card}\notready Let $n$ be a positive integer, let $F$ be a separably closed - field with $n$ nonzero in $F$, and let $E$ be an elliptic curve over $F$. Then the $n$-torsion $E(K)[n]$ + field with $n$ nonzero in $F$, and let $E$ be an elliptic curve over $F$. Then the $n$-torsion $E(K)[n]$ in the $F$-points of $E$ is a finite group of size $n^2$. \end{theorem} \begin{proof} @@ -22,7 +22,7 @@ \section{The arithmetic of elliptic curves} This theorem actually tells us the structure of the $n$-torsion, because of the following purely group-theoretic result: \begin{lemma}\label{group_theory_lemma}\lean{group_theory_lemma} - Say $n$ is a positive integer, $r$ is a natural, and $A$ is an abelian group. Assume that for all $d\mid n$, the $d$-torsion $A[d]$ of $A$ has size $d^r$. Then $A[n]\cong (\Z/n\Z)^r$. + Say $n$ is a positive integer, $r$ is a natural, and $A$ is an abelian group. Assume that for all $d\mid n$, the $d$-torsion $A[d]$ of $A$ has size $d^r$. Then $A[n]\cong (\Z/n\Z)^r$. \end{lemma} \begin{proof} The result is obvious if $n=1$, so we may assume $n>1$. One proof would be to write $A$ as $\prod_{i=1}^t(\Z/a_i\Z)$ @@ -31,7 +31,7 @@ \section{The arithmetic of elliptic curves} \begin{corollary}\label{Elliptic_curve_n_torsion_2d}\lean{EllipticCurve.n_torsion_dimension} Let $n$ be a positive integer, let $F$ be a separably closed - field with $n$ nonzero in $F$, and let $E$ be an elliptic curve over $F$. Then the $n$-torsion $E(F)[n]$ + field with $n$ nonzero in $F$, and let $E$ be an elliptic curve over $F$. Then the $n$-torsion $E(F)[n]$ in the $F$-points of $E$ is a finite group isomorphic to $(\Z/n\Z)^2$. \end{corollary} \begin{proof}\uses{group_theory_lemma,EllipticCurve.n_torsion_card} @@ -52,8 +52,8 @@ \section{Good reduction} We give a brief overview of the theory of good and multiplicative reduction of elliptic curves. For more details one can consult the standard sources such as~\cite{silverman1}. We stick with the low-level approach, thinking of elliptic curves as plane cubics; whilst we cannot do this forever, it will suffice for these initial results. -\begin{definition}\label{EllipticCurve.GoodReduction} Let $E$ be an elliptic curve over the field of fractions $K$ of a valuation ring $R$ with maximal ideal $\m$. We say $E$ has \emph{good reduction over $R$} if $E$ has a model with -coefficients in $R$ and the reduction mod $\m$ is still non-singular. If $E$ is an elliptic curve +\begin{definition}\label{EllipticCurve.GoodReduction} Let $E$ be an elliptic curve over the field of fractions $K$ of a valuation ring $R$ with maximal ideal $\m$. We say $E$ has \emph{good reduction over $R$} if $E$ has a model with +coefficients in $R$ and the reduction mod $\m$ is still non-singular. If $E$ is an elliptic curve over a number field $N$ and $P$ is a maximal ideal of its integer ring $\calO_N$, then one says that $E$ has \emph{good reduction at $P$} if $E$ has good reduction over the $\calO_{N,P}$, the localisation of $\calO_N$ at $P$. \end{definition} @@ -66,7 +66,7 @@ \section{Good reduction} \end{lemma} \begin{proof} The reduction mod $p$ of the equation defining the Frey curve is still a smooth plane cubic, because the three roots $0$, $a^\ell$ and $-b^\ell$ are distinct modulo $p$ - (note that the difference between $a^\ell$ and $-b^\ell$ is $c^\ell$). + (note that the difference between $a^\ell$ and $-b^\ell$ is $c^\ell$). \end{proof} If $E$ is an elliptic curve over a number field $N$ and if $\rho$ is the representation @@ -81,7 +81,7 @@ \section{Good reduction} is a working definition. \begin{definition}\label{finite_flat_group_scheme} If $R$ is a commutative ring, then - a \emph{finite flat group scheme} over $R$ is the spectrum of a commutative Hopf algebra $H/R$ + a \emph{finite flat group scheme} over $R$ is the spectrum of a commutative Hopf algebra $H/R$ which is finite and flat as an $R$-module. \end{definition} @@ -89,8 +89,8 @@ \section{Good reduction} Some facts we will need are: -\begin{theorem}\label{good_reduction_implies_unramified}\notready If $E$ is an elliptic curve over a number - field $N$ and $E$ has good reduction at a maximal ideal $P$ of $\calO_N$, and if furthermore +\begin{theorem}\label{good_reduction_implies_unramified}\notready If $E$ is an elliptic curve over a number + field $N$ and $E$ has good reduction at a maximal ideal $P$ of $\calO_N$, and if furthermore $n\not\in P$, then the Galois representation on the $n$-torsion of $E$ is unramified. \end{theorem} \begin{proof} @@ -98,9 +98,9 @@ \section{Good reduction} is an etale finite flat group scheme. There might be simpler approaches however. It's worth looking to see what Silverman does. \end{proof} -\begin{theorem}\label{good_reduction_implies_flat}\uses{finite_flat_group_scheme}\notready If $E$ is an elliptic curve over a number field - $N$ and $E$ has good reduction at a maximal ideal $P$ of $\calO_N$ containing the prime number $p$, - then the Galois representation on the $p$-torsion of $E$ comes from a finite flat group scheme +\begin{theorem}\label{good_reduction_implies_flat}\uses{finite_flat_group_scheme}\notready If $E$ is an elliptic curve over a number field + $N$ and $E$ has good reduction at a maximal ideal $P$ of $\calO_N$ containing the prime number $p$, + then the Galois representation on the $p$-torsion of $E$ comes from a finite flat group scheme over the localisation $\calO_{N,P}$. \end{theorem} \begin{proof} @@ -115,7 +115,7 @@ \section{Multiplicative reduction} are both defined over $R/\m$, and \emph{non-split} otherwise. \end{definition} - If $E$ is an elliptic curve + If $E$ is an elliptic curve over a number field $N$ and $P$ is a maximal ideal of its integer ring $\calO_N$, then one says that $E$ has \emph{multiplicative reduction at $P$} if $E$ has multiplicative reduction over the $\calO_{N,P}$, the localisation of $\calO_N$ at $P$. \begin{lemma}\label{Frey_curve_mult_reduction}\uses{EllipticCurve.MultiplicativeReduction} If $E$ is the Frey curve $Y^2=X(X-a^\ell)(X+b^\ell)$ associated to a Frey @@ -123,7 +123,7 @@ \section{Multiplicative reduction} which divides $abc$, then $E$ has multiplicative reduction at~$p$. \end{lemma} \begin{proof} The hypothesis $p\mid abc$ implies that precisely two of the three roots $0$, $a^\ell$ and $-b^\ell$ - of the cubic are equal mod~$p$. Call $x\in\Z/p\Z$ this common value. Then the reduction mod $p$ of + of the cubic are equal mod~$p$. Call $x\in\Z/p\Z$ this common value. Then the reduction mod $p$ of the curve is smooth away from the point $(x,0)$, and has an ordinary double point at $(x,0)$. Hence the Frey curve has multiplicative reduction at $p$. @@ -133,13 +133,13 @@ \section{Multiplicative reduction} \end{remark} \begin{lemma}\label{Frey_curve_mult_reduction_at_two}\uses{EllipticCurve.MultiplicativeReduction} If $E$ is the Frey curve $Y^2=X(X-a^\ell)(X+b^\ell)$ associated to a Frey package - $(a,b,c,\ell)$ then $E$ has multiplicative reduction at 2. + $(a,b,c,\ell)$ then $E$ has multiplicative reduction at 2. \end{lemma} -\begin{proof} Indeed, the change of variables $X=4X'$ - and $Y=8Y'+4X'$ transforms the equation to +\begin{proof} Indeed, the change of variables $X=4X'$ + and $Y=8Y'+4X'$ transforms the equation to $64Y'^2+64X'Y'=64X'^3+16X'^2(b^\ell-a^\ell-1)-4X'a^\ell b^\ell$ and, because $\ell\geq5$, $b$ is even and $a=3$ mod 4, we see that the 64s cancel, giving an equation over $\Z$ which reduces mod 2 to - $Y'^2+X'Y'=X'^3+cX'^2$ for some $c\in\{0,1\}$. This cubic is smooth away from an ordinary + $Y'^2+X'Y'=X'^3+cX'^2$ for some $c\in\{0,1\}$. This cubic is smooth away from an ordinary double point at $(0,0)$. Hence the Frey curve has multiplicative reduction at~2. \end{proof} \begin{remark} Note that $E$ has split multiplicative reduction iff $c=0$, which happens iff $a^\ell=7$ mod $8$. We shall not need this fact. @@ -149,7 +149,7 @@ \section{Multiplicative reduction} multiplicative reduction at all primes. The main thing we need about elliptic curves with multiplicative reduction over nonarchimedean -local fields is the \emph{uniformisation theorem}, originally due to Tate. +local fields is the \emph{uniformisation theorem}, originally due to Tate. \begin{theorem}\label{Tate_curve_uniformisation}\uses{EllipticCurve.MultiplicativeReduction}\notready If $E$ is an elliptic curve over a field complete with respect to a nontrivial nonarchimedean (real-valued) norm $K$ and if $E$ has split @@ -166,7 +166,7 @@ \section{Multiplicative reduction} over a field $K$ complete with respect to a nontrivial nonarchimedean (real-valued) norm and with perfect residue field, and if $E$ has multiplicative reduction, then there's an unramified character $\chi$ of $\Gal(K^{\sep}/K)$ whose square is 1, such that for - all positive integers $n$ with $n\not=0$ in $K$, the + all positive integers $n$ with $n\not=0$ in $K$, the $n$-torsion $E(K^{\sep})[n]$ is an extension of $\chi$ by $\epsilon\chi$, where $\epsilon$ is the cyclotomic character. Furthermore, the element of $K^\times/(K^\times)^\ell$ corresponding to this extension is given by the $q$-invariant of the curve. @@ -182,7 +182,7 @@ \section{Hardly ramified representations} We make the following definition; this is not in the literature but it is a useful concept for us. \begin{definition}\label{hardly_ramified}\notready Let $\ell\geq5$ be a prime and let $V$ be a - 2-dimensional vector space over $\Z/\ell\Z$. A representation + 2-dimensional vector space over $\Z/\ell\Z$. A representation $\rho: \GQ\to \GL(V)$ is said to be \emph{hardly ramified} if it satisfies the following four axioms: \begin{enumerate} \item $\det(\rho)$ is the mod $\ell$ cyclotomic character; @@ -192,12 +192,12 @@ \section{Hardly ramified representations} \end{enumerate} \end{definition} -We are interested in hardly ramified representations for several reasons. One is that by using some -deep theorems, we will be able to prove that all hardly ramified representations are -\emph{potentially automorphic}, which will give us our first foothold into the world of modular +We are interested in hardly ramified representations for several reasons. One is that by using some +deep theorems, we will be able to prove that all hardly ramified representations are +\emph{potentially automorphic}, which will give us our first foothold into the world of modular forms. We shall come back to these ideas later. In the next section we shall be concerned with the following rather simpler result, namely that the $\ell$-torsion in the Frey curve -associated to a Frey package $(a,b,c,\ell)$ is hardly ramified. The proof is standard; +associated to a Frey package $(a,b,c,\ell)$ is hardly ramified. The proof is standard; for another reference, see Theorem~2.15 of~\cite{ddt}. \section[The l-torsion in the Frey curve is hardly ramified.]{The $\ell$-torsion in the Frey curve is hardly ramified.} @@ -208,11 +208,11 @@ \section{Hardly ramified representations} \begin{theorem}\label{Frey_curve_good}\notready If $p\not=\ell$ is a prime not dividing $abc$ then $\rho$ is unramified at~$p$. \end{theorem} - \begin{proof}\uses{Frey_curve_good_reduction,good_reduction_implies_unramified} Indeed, $E$ has good reduction at $p$, and hence $\rho$ is unramified at $p$ - by~\ref{good_reduction_implies_unramified}. + \begin{proof}\uses{Frey_curve_good_reduction,good_reduction_implies_unramified} Indeed, $E$ has good reduction at $p$, and hence $\rho$ is unramified at $p$ + by~\ref{good_reduction_implies_unramified}. \end{proof} -If however $p$ divides $abc$ then $E$ has multiplicative +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}\lean{FLT.FreyPackage.FreyCurve.j}\leanok\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$. @@ -224,7 +224,7 @@ \section{Hardly ramified representations} \begin{corollary} \label{FLT.FreyPackage.FreyCurve.j_valuation_of_bad_prime} - \lean{FLT.FreyPackage.FreyCurve.j_valuation_of_bad_prime} + \lean{FLT.FreyPackage.FreyCurve.j_valuation_of_bad_prime} \uses{Frey_curve_j}\leanok If $(a,b,c,\ell)$ is a Frey package and the $j$-invariant of the corresponding Frey curve is $j$, and if $2 0$ by working locally on the base, so $G$ is contained in $A[n]$. Then - $n: A \to A$ is the fppf quotient of the source by $A[n]$, so it expresses $A$ as an - $A[n]$-torsor over itself. The problem of building $A/G$ as an abelian scheme is then + Brian Conrad suggested the following approach, applicable as well for abelian schemes $A\to S$ + over a base. Let $G$ be a finite locally free $S$-subgroup of $A$, say $G$ with constant + rank $n > 0$ by working locally on the base, so $G$ is contained in $A[n]$. Then + $n: A \to A$ is the fppf quotient of the source by $A[n]$, so it expresses $A$ as an + $A[n]$-torsor over itself. The problem of building $A/G$ as an abelian scheme is then seen to be the β€œsame” as that of constructing the quotient of this $A[n]$-torsor by the G-action. - In other words, the problem them becomes one having nothing specific to do with abelian schemes, - at the cost of working over a base (such as the original target $A$) even when $S$ was the - spectrum of a field in the application. The question is now: for a finite locally free - commutative $S$-group $H$ and a closed locally free $S$-subgroup $G$, build a reasonable quotient - $H/G$. One approach is to look at the Cartier dual $H^\vee\to G^\vee$, show that it's faithfully - flat, and then deduce that the Cartier dual of the kernel of this map does the job. Note that - one input for this proof is the claim that inclusions of Hopf algebras over fields are flat, + In other words, the problem them becomes one having nothing specific to do with abelian schemes, + at the cost of working over a base (such as the original target $A$) even when $S$ was the + spectrum of a field in the application. The question is now: for a finite locally free + commutative $S$-group $H$ and a closed locally free $S$-subgroup $G$, build a reasonable quotient + $H/G$. One approach is to look at the Cartier dual $H^\vee\to G^\vee$, show that it's faithfully + flat, and then deduce that the Cartier dual of the kernel of this map does the job. Note that + one input for this proof is the claim that inclusions of Hopf algebras over fields are flat, proved nicely in Waterhouse’s book. \end{proof} @@ -414,7 +414,7 @@ \section{Hardly ramified representations} \end{corollary} \begin{proof}\uses{Elliptic_curve_quotient_by_finite_subgroup, mazur} $\rho$ has a Galois-stable submodule $C$. The quotient curve $E/C$ now has a trivial 1-dimensional submodule, and also three points of order~2 (the images of the three - 2-torsion points in $E$). Hence the torsion subgroup of $E/C$ has order at least $4\ell\geq 20$, + 2-torsion points in $E$). Hence the torsion subgroup of $E/C$ has order at least $4\ell\geq 20$, again contradicting Mazur's theorem. \end{proof} diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 306819c0..6c00e084 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -8,6 +8,7 @@ %\input{chapter/ch06automorphicrepresentations} -- all in mathlib or on the way. \input{chapter/ch07exampleGLn} \input{chapter/FrobeniusProject} +\input{chapter/AdeleMiniproject} \input{chapter/QuaternionAlgebraProject} \input{chapter/chtopbestiary} \input{chapter/biblio}