Miniproject: Haar characters

Stream: FLT

[Kevin Buzzard]

There's a new miniproject up in the blueprint (only): Haar characters. Issues on the project dashboard will be forthcoming.

The reason they're not there already is that now my thoughts on what I need are coherent (after going through the finite-dimensionality of quaternionic modular forms proof), I realise that I need something more general than these characters $R^\times\to\R_{>0}$, I need the more general concept of the scaling factor of a continuous isomorphism $\phi:(A,+)\cong(A,+)$ where $\phi$ is a homeomorphism. Right now it looks like I'd have to beef up $\phi$ to be a generator of some (multiplicative) $\Z$ which could then act on $A$ which seems a bit daft. Conversely the exact structure I want (additive homeomorphisms) doesn't seem to exist in mathlib, although it looks like it's on the way in #16991 . This issue is currently blocking my being able to open a bunch more issues for the dashboard. @Yaël Dillies what do you think? Should I wait for #16991 ? This is my gut instinct. The point is that this more general notion of scaling factor is now playing a bigger role (for example there are situations where I don't want to prove that $R$ is a ring but still want to talk about the Haar character, and there are situations in the application where I need to think about right not left multiplication in the non-commutative setting, which is still an additive iso $(R,+)\cong (R,+)$.

[Yaël Dillies]

Kevin Buzzard said:

I realise that I need something more general than these characters $R^\times\to\R_{>0}$, I need the more general concept of the scaling factor of a continuous isomorphism $\phi:(A,+)\cong(A,+)$ where $\phi$ is a homeomorphism.

Sure, that's easy enough to do. Maybe @Andrew Yang and I can do it next monday.

Kevin Buzzard said:

it looks like it's on the way in #16991 . This issue is currently blocking my being able to open a bunch more issues for the dashboard. Yaël Dillies what do you think? Should I wait for #16991 ?

#16991 is the kind of PRs that should be straightforward to get in, so I'd sat wait. Alternative trick: Use continuous Z-linear isos.

Kevin Buzzard said:

The point is that this more general notion of scaling factor is now playing a bigger role (for example there are situations where I don't want to prove that $R$ is a ring but still want to talk about the Haar character, and there are situations in the application where I need to think about right not left multiplication in the non-commutative setting, which is still an additive iso $(R,+)\cong (R,+)$.

I don't quite understand this motivation. All we need is some group G acting by continuous add isos on some topological group A. In particular:

• G needn't act by left multiplication, right multiplication is fine
• We don't need to make R into a topological ring before letting R\^x act on R

[Yaël Dillies]

TLDR: We can do what you asked, but did you really ask for the right thing?

[Kevin Buzzard]

What I'm saying is that in my revised development of the theory, the concept of "real number associated to an automorphism of a topological additive group" plays a far more prominent role than before, when I was more focussed on "real number associated to a unit in a topological ring" (and thought that I could get away with nothing but this).

[Kevin Buzzard]

You developed the theory of "real number associated to an element of a group acting on an additive abelian group" (which was what I asked you to do) but I now find myself in situations where I don't even have the group, just a continuous isomorphism of a locally compact topological abelian group.

[Kevin Buzzard]

I'm spending the next couple of days focussed on Haar characters. I'm now almost completely happy with the LaTeX writeup in the blueprint, but there are several blueprint lemmas which don't even have labels so are not even on the graph, the blueprint graph itself is totally disconnected, and over half of the results discussed in the LaTeX have no corresponding Lean statements.

The main results we need for finite-dimensionality of automorphic forms in this miniproject are: (1) continuity of the Haar character on units of a ring (see here), (2) invertible linear maps scale Haar measure by the character of their determinant (see here), (3) a purely algebraic result saying that left and right multiplication by elements of a central simple algebra over a field have the same determinant (see here) and (4) haar character of restricted product is is product of haar characters (see here). Of these, we only have a Lean statement for the first, but right now my priority is writing Lean statements for everything in the miniproject, and updating the blueprint to make it a connected component of blue and green like all good blueprints should be.

As well as these "flagship" results, we need plenty of smaller ones to get us there, and I've just formalized a bunch of sorries on this finer invariant (the positive real associated to an additive homeomorphism $\phi$ of a locally compact abelian additive topological group $A$). I call it $d_A(\phi)$ in the LaTeX and addEquivAddHaarChar in the LaTeX. There are two new files FLT/HaarMeasure/HaarChar/AddEquiv.lean and FLT/HaarMeasure/HaarChar/Ring.lean each containing about 6 sorries, some of them pretty straightforward. I am currently a bit confused about whether I should open github tasks saying "fill in all of the sorries in this file" or just saying "fill in one sorry in this file". Before I open any issues at all, let's experiment with basically the same method which other formalization projects use, which is that I'll just post the sorries here in this thread. I'll post them as individual posts; if you want to claim one then react with a silly emoji.

Tasks are below here!

Let's start off with the file FLT/HaarMeasure/HaarChar/AddEquiv.lean.

[Kevin Buzzard]

• First sorry is isHaarMeasure_comap: pullback of Haar measure along a topological group isomorphism is a Haar measure.

[Kevin Buzzard]

• Second sorry is mulEquivHaarChar_eq: the positive real associated to an additive homeomorphism of a locally compact abelian group is independent of the choice of Haar measure. This should follow from docs#MeasureTheory.Measure.haarScalarFactor_eq_mul

[Kevin Buzzard]

• Third sorry is addEquivAddHaarChar_mul_integral: Pulling back Haar measure along the isomorphism scales integrals by the fudge factor. Proof is that the comapped measure is just a scalar multiple of the original measure. Same proof will work for 4th sorry mulEquivHaarChar_mul_integral so the challenge is either to do them both or to get to_additive working.

[Kevin Buzzard]

• 5th and 6th sorries are the additive and multiplicative versions of addEquivAddHaarChar_mul_volume, which says that this fudge factor is how the measure is scaled on measurable sets. Probably follows from the definition, or the previous sorries.

[Kevin Buzzard]

• 7th and 8th sorries are id and comp for the fudge factor; fudge factor of identity iso is 1, fudge factor of composite is product of fudge factors. [edit: 7 done, 8 still open]

[Kevin Buzzard]

Now onto the file FLT/HaarMeasure/HaarChar/Ring.lean.

• First two sorries are in mulLeft and they're the statement that left multiplication by an element of a topological ring is continuous. They might both be exact? or fun_prop or something? Should follow easily from the axioms of a topological ring though.

[Kevin Buzzard]

• Next sorry might be challenging. It's ringHaarChar_continuous, the challenge to formalise Sebastien Gouezel's proof that the fudge factor, considered as a function $R^\times\to\R_{\geq0}$, is continuous. The LaTeX proof is in the blueprint and in the Lean file.

[Kevin Buzzard]

• Next two are much easier; they're to show that the fudge factor (now called ringHaarChar is a group hom; this follows from results in the earlier file.

[Kevin Buzzard]

• The next sorry is ringHaarChar_mul_integral which should easily follow from addEquivAddHaarChar_mul_integral.

[Kevin Buzzard]

• And the final sorry for now is ringHaarChar_mul_volume which should hopefully follow easily from addEquivAddHaarChar_mul_volume.

[Kevin Buzzard]

I am going to press on making more sorries and hopefully within the next two days I will have got all of the statements of the results of this miniproject into Lean form.

[Edison Xie]

Kevin Buzzard said:

(3) a purely algebraic result saying that left and right multiplication by elements of a central simple algebra over a field have the same determinant (see here)

Claiming this (after exam) if no one else want it :)

[Kevin Buzzard]

By Thursday I'll have a formal statement for you. Sadly I need to pause this work right now to write a reference and open my emails, so it's unclear when I'll be back today.

[Edison Xie]

I could write the statement myself and have you check it's correct :-)

[Kevin Buzzard]

I'd prefer to do that myself while you're revising for your exams!

[Kevin Buzzard]

I finally finished my review of the Haar character miniproject. As a consequence the blueprint graph of this miniproject https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_chapter_9.html is now connected and all LaTeX statements have Lean counterparts. I have thrown in some new sorries into the code with no associated tasks because I just wanted to get the blueprint connected before Monday. Hopefully I'll find time to open tasks explaining exactly what needs to be done soon.