Outstanding Tasks, V6: adeles, measures, quaternion alg...

Stream: FLT

[Kevin Buzzard]

People have been getting on with things and I've been managing stuff on the project dashboard. But it was suggested to me that I should advertise what's going on currently, so here's a round-up of where we are, where we're going, and what needs doing.

The big picture: Andrew Yang has finished formalizing an "abstract" R=T theorem :tada: (this is a pure commutative algebra statement) and we now need to give definitions of the rings R (a deformation ring) and T (a Hecke algebra) which we will use in the application of this theorem. These two goals are also very much do-able; I am working on T, and Javier Lopez Contreras is working on R (if anyone wants to review FLT#346 and FLT#347 then please feel free; this is stuff which I could envisage ultimately ending up in mathlib, it is a basic and interesting example of representing a functor, but there are design decisions here which it would be wonderful to have some other eyes on). Once we have these rings, then FLT will be reduced to two major tasks: (1) checking that the hypotheses of the R=T theorem are satisfied for the R and T that we've constructed and (2) checking that the conclusion of the theorem implies FLT. Once we have done this, a "bisection" of FLT will have occurred: instead of having to prove one very very very hard theorem, we will instead have to prove two very very hard but independent theorems.

[Kevin Buzzard]

One thing which I have achieved recently is what is hopefully a complete and coherent LaTeX write-up of part of the theory of automorphic forms which we will need for T (including many of the relevant definitions; one does not need to be an expert in the area to understand this part of the blueprint). This write-up spans four "mini-projects" -- the adele miniproject, the Haar character miniproject, the Fujisaki lemma miniproject and the quaternionic modular forms miniproject. Put together, these four projects will show that certain spaces of automorphic forms are finite-dimensional, which will imply various finiteness results about the Hecke algebras T which are inputs to the R=T theorem (a Hecke algebra is just a certain ring of endomorphisms of a space of automorphic forms, at least in this context).

In particular, although I am still a long way from a full LaTeX write-up of what we're doing, hopefully we have a coherent and complete LaTeX write-up of the proof that certain spaces of quaternionic modular forms are finite-dimensional.

In the next four posts I'll summarise what needs doing in each of the four miniprojects.

[Kevin Buzzard]

The adele miniproject: what is needed here are results about number fields and their completions. Some of them are phrased in terms of adeles (which are some kind of product of all the completions of a number field, for example the adeles of $\mathbb{Q}$ are a subring of $\mathbb{R}\times\prod_p\mathbb{Q}_p$ containing the open subring $\mathbb{R}\times\prod_p\mathbb{Z}_p$) but at the end of the day what we need is really just results about number fields and their completions.

You can see in the blueprint what needs doing (it's the things without ticks). But let me highlight the key jobs.

Theorem 8.4 is a trivial consequence of the claim that any two norms on a finite-dimensional vector space over a complete field are equivalent. I think I occasionally ask whether we have this, but we need it for the $p$-adic numbers, not just the reals.

Theorem 8.6 is probably the most mathematically challenging result here. It is the claim that if $L/K$ is a finite extension of number fields and $v$ is a finite place of $K$, then the natural map $L\otimes_KK_v\to \prod_{w|v}L_w$ is an isomorphism. I've written a detailed proof in the blueprint.

Theorem 8.7 and Theorem 8.8 are easy consequences.

Theorem 8.9 has some content: it is that the isomorphism $L\otimes_KK_v=\prod_wL_w$ induces an isomorphism integrally for all but finitely many places. Again there's a detailed informal proof in the blueprint.

I skipped the proof of Theorem 8.13, I didn't make a plan for it yet because I don't know enough about infinite completions yet. It's the statement that $L\otimes_KK_\infty=L_\infty$ both topologically and algebraically, with $K_\infty:=\prod_{v|\infty}K_v$.

Theorems 8.14 and 8.15 are easy consequences of earlier results.

Much of the above is adele-free; here are the adele results which we need.

FLT#253 is the claim that the adeles of a number field are locally compact. Mercuri has proved this in his adeles repo, so it's just a case of upstreaming.

Theorem 8.16 to 8.20 show that $K$ is discrete in $\mathbb{A}_K$ and that the quotient $\mathbb{A}_K/K$ is compact. My proposal is to prove this explicitly for $K=\mathbb{Q}$ and then deduce it from the above results about base change for adeles.

[Kevin Buzzard]

Next the Haar character project. During my LaTeX write-up I decided that the fundamental definition should be this: if $(A,+)$ is a locally compact topological abelian additive group and if $\phi:A\cong A$ both a topological and group-theoretic isomorphism, then there is a positive real number $d_A(\phi)$ associated to $\phi$ which records the amount that $A$'s additive Haar measure is scaled by $\phi$. A far more detailed exposition is in the blueprint. There are a bunch of fun things still missing here. Here are some examples.

Theorem 9.5 is the following claim: if $R$ is a locally compact topological ring then multiplication by $u\in R^\times$ gives rise to an automorphism $\phi = x\mapsto ux$ of $(R,+)$ as above, and hence a positive real $\delta(u):=d_R(\phi)$. The claim is that this map is continuous, and Sebastien Gouezel provided a proof on Zulip which I have dutifully transcripted in the blueprint.

Lemma 9.6 is the claim that an automorphism of a finite-dimensional vector space over a locally compact topological field changes Haar measure by a factor determined by the determinant of the matrix. I propose a proof in the blueprint.

9.8 to 9.15 are all basic API for the maps $d_A$ and $\delta_R$. Complete LaTeX proofs are in the blueprint.

9.16 to 9.19 are more theoretically complex results involving the behaviour of these concepts under infinite restricted products. Anatole Dedecker is currently in the process of PRing infinite restricted products to mathlib https://github.com/leanprover-community/mathlib4/pull/20021 so we might want to wait on this (or give Anatole a hand). This is all straightforward algebra and topological algebra and represents a bit of a bottleneck because it's a huge draft PR so I can see it being a while before it makes it into mathlib.

[Kevin Buzzard]

Fujisaki's lemma is the name which John Voight gives to a certain finiteness result in the theory of division algebras over global fields. It is a huge generalization of two results in classical number theory, namely finiteness of the class group of a number field, and the formula for the rank of the unit group of the integers of a number field. I'm not sure how much of the proof will be reusable but I have written up what is hopefully a coherent strategy in the blueprint, although I have barely begun to think about the Lean side of things. The proof is making a bunch of intermediate definitions and proving slightly fiddly things about them. It could perhaps be made constructive but I am not sure I am interested in doing this; all we need for FLT is the finiteness statement.

[Kevin Buzzard]

Finally the quaternionic modular forms project. The blueprint contains a definition of quaternionic modular forms. The claim is that these spaces are finite-dimensional, and the proof is "follows immediately from Fujisaki's lemma". However I am wondering whether we should just make our lives easier and restrict to weight 2 modular forms, as these are the only things which are needed for FLT.

[Ruben Van de Velde]

Finite {w : HeightOneSpectrum B // v = comap A w} is supposed to be true, right?

[Kevin Buzzard]

Yes that's true for all Dedekind domains I should think, when L/K is finite and separable.

[Ruben Van de Velde]

I left it as a sorry in FLT#353

[Andrew Yang]

Should be easy from docs#primesOver_finite

[Ruben Van de Velde]

That works assuming NoZeroSMulDivisors A B - can I assume that? :)

[Kevin Buzzard]

A is a subring of a field K and B is a subring of a field L with $K\subseteq L$ so presumably this can be proved?

[Yakov Pechersky]

import Mathlib

variable (A K L B : Type*) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra B L]
    [Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
    [IsFractionRing B L]

example : NoZeroSMulDivisors A B := by
  constructor
  intro r x h
  suffices (algebraMap A K r) • (algebraMap B L x) = 0 by
    rw [smul_eq_zero] at this
    simpa using this
  have ht : Algebra.linearMap B L (r • x) = r • algebraMap B L x := by
    simp [LinearMap.map_smul_of_tower]
  rw [IsScalarTower.algebraMap_smul, ← ht, h, map_zero]

[Ruben Van de Velde]

Can't argue with that!

[Ruben Van de Velde]

I'm now confused about the start of the proof of theorem 8.8: we have an $L$-algebra isomorphism, but where does the $K_v$-algebra isomorphism come from?

[Andrew Yang]

The blueprint isn't clear about this but the map is also $K_v$ linear by construction.

[Kevin Buzzard]

Each $L_w$ is a $K_v$-module (see Theorem 8.4). It's very frustrating that $A\otimes B$ can't be both an $A$-module and a $B$-module in Lean because Eric will point out that if $A=B$ then we get a diamond, so in all the cases where $A\not=B$ we have to jump through hoops to make this both an $A$-module and a $B$-module. Eric initially suggested that I carefully choose whether I write $A\otimes B$ or $B\otimes A$ depending on which thing I wanted the product to be a module over, but after trying this for a while I realised that the answer was that I want $A\otimes B$ to be both an $A$-module and a $B$-module so this hack was not going to work. The solution now is to make that def which makes it whichever thing it's not a module for by default, into a local instance.

[Yaël Dillies]

What about having a RightTensorAct type synonym and an instance Module (RightTensorAct B) (A tensor B) on top of the existing Module A (A tensor B) instance?

[Yaël Dillies]

Then you get any issue because the two actions on A tensor A are by A and RightTensorAct A, which are different

[Kevin Buzzard]

But $L$ and $K_v$ are also different, and in all the applications in FLT so far $A$ and $B$ are different, so it's much easier just to make the other module def locally an instance.