MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one

Stream: FLT

[Kevin Buzzard]

I feel like we're nearly there with the big finite-dimensionality result, but I don't think we're going to make it by 2025. I suspect that the hardest part of what is left is MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one whose proof in FLT#820 is kind of spiralling out of control. Let me summarise why this has become messy to formalize (at least the way I'm trying to formalize it). First let me state the result.

We have $V$ a finite-dimensional $\mathbb{Q}$-vector space and $\phi:V\cong V$ a $\mathbb{Q}$-linear isomorphism. Let $\mathbb{A}$ denote the adeles of $\mathbb{Q}$. Then $V_{\mathbb{A}}:=V\otimes_{\mathbb{Q}}\mathbb{A}$ is a finite free $\mathbb{A}$-module; give it the $\mathbb{A}$-module topology (which is just the product topology if you pick a basis). This makes $V_{\mathbb{A}}$ into a locally compact additive abelian group. The claim is that the continuous endomorphism $\phi_{\mathbb{A}}$ of $V_{\mathbb{A}}$ induced by $\phi$ has Haar character 1 (i.e. it scales additive Haar measure by a factor of 1). Here's a short and simple proof: $\phi_{\mathbb{A}}=\prod_v\phi_v$ where $\phi_v$ is the associated endomorphism of $V_v:=V\otimes_{\mathbb{Q}}\mathbb{Q}_v$, and we have formal proofs of all of the following facts: the Haar character of $\prod_v\phi_v$ is just the product of the Haar characters of the $\phi_v$ (this is a finite product as all but finitely many of the local Haar characters are 1), the Haar character of $\phi_v$ is just $|det(\phi)|_v$, and $det(\phi)\in\mathbb{Q}^\times$ so the result now follows from the product formula.

The thing which has become a nightmare is manipulating $V\otimes_{\mathbb{Q}}\mathbb{A}$. There are two things being swept under the carpet here. First, we want to commute the tensor product with the restricted product (which we can do thanks to Maddy Crim's work). But the restricted product is over subspaces $\mathbb{Z}_p\subseteq\mathbb{Q}_p$ which are not $\mathbb{Q}$-modules, so instead of working with $V\otimes_{\mathbb{Q}}$ we need to work with $\Lambda\otimes_{\mathbb{Z}}$ where $\Lambda$ is a random $\mathbb{Z}$-lattice in $V$. I have developed enough of the theory of lattices in FLT#820 to make all of this possible, but am continually having to write down continuous linear isomorphisms $V\otimes_{\mathbb{Q}}\mathbb{A}=\Lambda\otimes_{\mathbb{Z}}\mathbb{A}=\Lambda\otimes_{\mathbb{Z}}\mathbb{Q}_\infty\times\prod'_p[\Lambda\otimes_{\mathbb{Z}}\mathbb{Q}_p;\Lambda\otimes_{\mathbb{Z}}\mathbb{Z}_p]=V\otimes_{\mathbb{Q}}\mathbb{Q}_\infty\times\prod'_p[V\otimes_{\mathbb{Q}}\mathbb{Q}_p;im(\Lambda\otimes_{\Z}\mathbb{Z}_p)]$ and there is at least one of these obvious equalities where continuity is not immediate; the fact that I am constantly having to put in symms to deal with left/right actions on tensor products is making things worse. I will plough on though(edit: I will actually try a different approach). I am unlikely to get much done 1st to 4th because of family commitments but that's where we are right now.

Another approach would be to simply prove a generalisation of Lemma 9.18, the statement that if $\phi$ is an automorphism of a finite-dimensional vector space over a locally compact field then the Haar character of $\phi$ equals the Haar character of $det(\phi)$: if we had this for automorphisms of finite free modules over locally compact commutative rings then this would be enough. But I'm not sure I know a proof of this for locally compact rings. The proof I know for fields involves writing an arbitrary automorphism as a product of certain elementary matrices, and for a general ring there's an obstruction to doing this which lies in a K-group. Just writing this now makes me wonder however whether I should try this alternative approach.

It's kind of annoying, but I think the following is false: if $R\subseteq A$ are locally compact commutative rings and $R$ has the subspace topology, then Haar characters commute with the inclusion. I can only prove this if the inclusion is an open immersion and this is not the case for $\mathbb{Q}\subseteq\mathbb{A}$.

[Kevin Buzzard]

OK I am switching to plan B in FLT#822 which starts by generalizing many of the results of FLT/HaarMeasure/HaarChar/FiniteDimensional.lean to commutative topological rings. In retrospect I think this will be a lot less painful.

I'll define a predicate on automorphisms of finite free modules saying "I am a product of transvections and diagonal matrices", prove that it's true for modules over a field (this is in mathlib) and stable under base change, and then generalize lemma 9.18 (now 10.18 now Frobenius is back) to rings and this will be enough (because the endomorphism we're interested in is a base change from a field).

[Kevin Buzzard]

Wooah that went much better than expected. All of the proofs generalized immediately after adding in the assumption. Maybe 2025 is back on (although I am going to be dragged away from this computer in a few hours and forced to celebrate something or other :-/ )

[Kevin Buzzard]

OK so indeed FLT#822 removes the sorry, and there are several lessons learnt.

Firstly, writing here about my problems was a way of rubber-ducking them away: whilst writing I found another approach, so thanks to the community for that!

Secondly, in the FLT PR which proved that an automorphism of a finite-dimensional vector space over a locally compact field scaled Haar meaasure by the determinant, we should have worked over commutative rings and assumed that the matrix of the automorphism was a product of transvections and diagonal matrices (something which is automatically true over fields but which is not true in general; there is an obstruction if $K_1(R)$ is strictly bigger than $R^\times$ which as far as I know can happen). However the changes were trivial to make because none of the proofs broke; this was exactly the dream scenario in formalization where you make the statement more general and the proof just goes through. Probably I should PR the generalization to mathlib.

Thirdly, I realised that actually there's a mathematical question which is unresolved here; I've just asked it on mathoverflow. Before I attempt to refactor mathlib it would be nice to know what the answer is.