Fermat's Last Theorem Blueprint

14. Appendix: A collection of results which are needed in the proof.🔗

14.1. Results from class field theory🔗

Theorem14.1
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Definition 14.2
Blueprint label
  • local_Weil_group
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

The maximal unramified extension K^{un} in a given algebraic closure of K is Galois over K with Galois group "canonically" isomorphic to \widehat{\Z} in two ways; one of these two isomorphisms identifies 1\in\widehat{\Z} with an arithmetic Frobenius, the endomorphism inducing x\mapsto x^q on the residue field of K^{un}, where q is the size of the residue field of K. The other identifies 1 with geometric Frobenius, defined to be the inverse of arithmetic Frobenius.

Definition14.2
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Theorem 14.1 The topological group described above is called the Weil group of K.

Theorem14.3
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Definition 14.2 If K is a finite extension of \Q_p, then there are two canonical isomorphisms of topological abelian groups between K^\times and the abelianization of the Weil group of K.

Proof

This is the main theorem of local class field theory; see for example the relevant articles in the cited class-field-theory references or many other places.

Theorem14.4
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

If M is finite then the cohomology groups H^i(G_K,M) are all finite.

Theorem14.5
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

If M is torsion then H^i(G_K,M)=0 if i>2.

Theorem14.6
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

H^2(G_K,\mu_n) is canonically isomorphic to \Z/n\Z.

Theorem14.7
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

If \mu=\bigcup_{n\geq1}\mu_n and M':=\Hom(M,\mu) is the dual of M, then for 0\leq i\leq 2 the cup-product pairing H^i(G_K,M)\times H^{2-i}(G_K,M')\to H^2(G_K,\mu)=\Q/\Z is perfect.

Theorem14.8
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

If h^i(M) denotes the order of H^i(G_K,M), then h^0(M)-h^1(M)+h^2(M)=0.

Theorem14.9
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Theorem 14.3 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 \Gamma_N^{ab}; one sends local uniformizers to arithmetic Frobenii and the other to geometric Frobenii, and each is compatible with the local isomorphisms above.

Proof

This is the main theorem of global class field theory; see for example Tate's article in the cited class-field-theory references.

Theorem14.10
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Theorem 14.9 Let S be a finite set of places of a number field K. For each v \in S let L_v/K_v be a finite Galois extension. Then there is a finite solvable Galois extension L/K such that if w is a place of L dividing v \in S, then L_w/K_v is isomorphic to L_v/K_v as a K_v-algebra. Moreover, if K^{\avoid}/K is any finite extension then L can be chosen linearly disjoint from K^{\avoid}.

14.2. Structures on the points of an affine variety.🔗

All rings and algebras in this section are commutative with a 1, and all morphisms send 1 to 1.

Let X = \Spec(A) be an affine scheme of finite type over a field K. For example X could be an affine algebraic variety; in fact we shall only be interested in smooth affine varieties in the applications, but the initial definition and theorem are fine for all finite type schemes.

If R is any K-algebra then one can talk about the R-points X(R) of X, which in this case naturally bijects with the K-algebra homomorphisms from A to R.

Definition14.11
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

If X is an affine scheme of finite type over K, and if R is a K-algebra which is also a topological ring, then we define a topology on the R-points X(R) of X by embedding the K-algebra homomorphisms from A to R into the set-theoretic maps from A to R with its product topology, and giving it the subspace topology.

Theorem14.12
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

If X is as above and X \to \mathbb{A}^n_K is a closed immersion, then the induced map from X(R) with its topology as above to R^n is an embedding of topological spaces (that is, a homeomorphism onto its image). This uses Definition 14.11.

Proof

We now specialise to the smooth case. I want to make the following conjectural definition:

Definition14.13
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Let K be a field equipped with an isomorphism to the reals, complexes, or a finite extension of the p-adic numbers. Let X be a smooth affine algebraic variety over K. Then the points X(K) naturally inherit the structure of a manifold over K.

Probably this is fine for a broader class of fields K.

Theorem14.14
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

If X is as in the previous definition and X \to \mathbb{A}^n_K is a closed immersion, then the induced map from X(K) with its manifold structure to K^n is an embedding of manifolds. This uses Definition 14.13.

Proof

I'm assuming this is standard, if true.

Corollary14.15
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

If G is an affine algebraic group of finite type over K=\R or K=\bbC then G(K) is naturally a real or complex Lie group. This uses Theorem 14.14.

The corollary, for sure, is true! And it's all we need. I have not yet made any serious effort to find a reference for the definition or independence, although there seem to be some ideas here. As a toy example, one can embed \GL_n(\R) into either \R^{n^2+1} via M \mapsto (M,\det(M)^{-1}) or into \R^{2n^2} via M \mapsto (M,M^{-1}) and the claim is that the two induced manifold structures are the same.

14.3. Algebraic groups.🔗

The concept of an affine algebraic group over a field K can be implemented in Lean as a commutative Hopf algebra over K, as a group object in the category of affine schemes over K, as a representable group functor on the category of affine schemes over K, or as a representable group functor on the category of schemes over K which is represented by an affine scheme. All of these are the same to mathematicians but different to Lean and some thought should go into which of these should be the actual definition, and which should be proved to be the same thing as the definition.

Definition14.16
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

An affine algebraic group G of finite type over a field k is said to be connected if it is connected as a scheme, and reductive if G_{\overline{k}} has no nontrivial smooth connected unipotent normal k-subgroup.

14.4. Automorphic forms and representations🔗

Definition14.17
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

A function f : G(N_\infty)\to\bbC is slowly-increasing if there exist some C>0 and n\geq1 such that |f(x)|\leq C||x||_\rho^n.

Theorem14.18
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Definition 14.17 This is independent of the choice of \rho as above.

Definition14.19
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀N
Used by 2
Hover a use site to preview it.
Preview
Definition 14.20
Blueprint label
  • cuspidal_automorphic_form
Uses target in
  • statement

Theorem 14.18 Definition 14.16 Corollary 14.15 Theorem 14.12 An automorphic form is a function \phi:G(\A_N)\to\bbC satisfying the following conditions.

  1. \phi is locally constant on G(\A_N^f) and C^\infty on G(N_\infty). In other words, for every g_\infty, \phi(-,g_\infty) is locally constant, and for every g_f, \phi(g_f,-) is smooth.

  2. \phi is left-invariant under G(N).

  3. \phi is right-U_\infty-finite, that is, the space spanned by x\mapsto \phi(xu) as u varies over U_\infty is finite-dimensional.

  4. \phi is right K_f-finite, where K_f is one, or equivalently all, compact open subgroups of G(\A_N^f).

  5. \phi is \mathcal{z}-finite, where \mathcal{z} is the centre of the universal enveloping algebra of the Lie algebra of G(N_\infty), acting via differential operators. Equivalently \phi is annihilated by a finite index ideal of this centre, so morally \phi satisfies many differential equations of a certain type.

  6. For all g_f, the function g_\infty\mapsto \phi(g_f g_\infty) is slowly-increasing in the sense above.

Definition14.20
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Definition 14.19 An automorphic form is cuspidal, or a cusp form, if it furthermore satisfies \int_{U(N)\backslash U(\A_N)}\phi(ux)\,du=0, where P runs through all the proper parabolic subgroups of G defined over N and U is the unipotent radical of P, and the integral is with respect to the measure coming from Haar measure.

Definition14.21
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀N
Used by 2
Hover a use site to preview it.
Preview
Definition 14.22
Blueprint label
  • automorphic_representation
Uses target in
  • statement

Definition 14.19 The group G(\A_N) acts on itself on the right, and this induces a left action of its subgroup G(\A_N^f)\times U_\infty on the spaces of automorphic forms and cusp forms. The Lie algebra \mathfrak{g} of G(N_\infty) also acts, via differential operators. Furthermore the actions of \mathfrak{g} and U_\infty are compatible in the sense that the differential of the U_\infty action is the action of its Lie algebra considered as a subalgebra of \mathfrak{g}. We say that the spaces are (G(\A_N^f)\times U_\infty,\mathfrak{g})-modules.

For non-cuspidal representations, they do not decompose as a direct sum; there is a continuous spectrum which decomposes as a direct integral. We may not ever need these. As a result the definition of an automorphic representation has to be slightly modified in the non-cuspidal case.

Definition14.22
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀N
Used by 2
Hover a use site to preview it.
Preview
Theorem 14.27
Blueprint label
  • automorphic_representation_local_decomposition
Uses target in
  • statement

Definition 14.21 An automorphic representation is an irreducible (G(\A_N^f)\times U_\infty,\mathfrak{g})-module isomorphic to an irreducible subquotient of the space of automorphic forms.

14.5. Galois representations🔗

14.6. Algebraic geometry🔗

Definition14.23
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

We need the definition of the canonical model over F of the Shimura curve attached to an inner form of \GL_2 with precisely one split infinite place, and likewise the Shimura surface associated to an inner form split at two infinite places and ramified elsewhere.

Theorem14.24
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Let K^{\avoid}/K be a Galois extension of number fields. Suppose also that S is a finite set of places of K, and for each v\in S let L_v/K_v be a finite Galois extension. Suppose also that T/K is a smooth, geometrically connected curve and that for each v\in S we are given a nonempty, \operatorname{Gal}(L_v/K_v)-invariant open subset \Omega_v\subseteq T(L_v). Then there is a finite Galois extension L/K and a point P\in T(L) with the prescribed local behavior.

Note that we do not even have the definition of a curve over a field in Lean.

14.7. Algebra🔗

Definition14.25
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Theorem 14.26 A cuspidal automorphic representation is an irreducible (G(\A_N^f)\times U_\infty,\mathfrak{g})-module isomorphic to an irreducible summand of the space of cusp forms.

Theorem14.26
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Definition 14.20 Definition 14.21 The cusp forms decompose as a typically infinite direct sum of irreducible (G(\A_N^f)\times U_\infty,\mathfrak{g})-modules.

Theorem14.27
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Definition 14.22 An irreducible admissible (G(\A_N^f)\times U_\infty,\mathfrak{g})-module is a restricted tensor product of irreducible representations \pi_v of G(N_v) as v runs through the finite places of N, tensored with a tensor product of irreducible (\mathfrak{g}_v,U_{\infty,v})-modules as v runs through the infinite places of N. The representations \pi_v are unramified for all but finitely many v.

Definition14.28
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Let N be a number field. A compatible family of d-dimensional Galois representations over N is a finite set of finite places S of N, a number field E, a monic degree d polynomial F_{\mathfrak p}(X)\in E[X] for each finite place \mathfrak p of K not in S, and, for each prime number \ell and field embedding \phi : E \to \overline{\mathbf{Q}}_\ell (or essentially equivalently for each finite place of E), a continuous homomorphism \rho:\operatorname{Gal}(\overline{K}/K)\to\GL_2(\overline{\mathbf{Q}}_\ell) unramified outside S and the primes of K above \ell, such that \rho(\operatorname{Frob}_{\mathfrak p}) has characteristic polynomial P_\pi(X) if \pi lies above a prime number p\neq \ell with p\not\in S.

Theorem14.29
Group: In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems. (28)
Hover another entry in this group to preview it.
Preview
Theorem 14.1
Blueprint label
  • «maximal_unramified_extension_of_p-adic_field»
Group
  • In this (temporary, unorganised) appendix we list a whole host of definitions and theorems which were known to humanity by the end of the 1980s and which we shall need. These definitions and theorems will find their way into more relevant sections of the blueprint once I have written more details. Note that some of these things are straightforward; others are probably multi-year research projects. The purpose of this chapter right now is simply to give the community (and possibly AIs) some kind of idea of the task we face. Note also that many of the definitions here are yet to be formalised in Lean, and this needs to be done before we can start talking about formalising theorems.
XL∃∀Nused by 1

Definition 14.22 Definition 14.23 Definition 14.28 Given an automorphic representation \pi for an inner form of \GL_2 over a totally real field and with reflex field E, such that \pi is weight 2 discrete series at every infinite place, there exists a compatible family of 2-dimensional Galois representations associated to \pi, with S the places at which \pi is ramified and F_{\mathfrak p}(X) the monic polynomial with roots the two Satake parameters for \pi at \mathfrak p.