Outstanding Tasks, V7 : Haar characters

Stream: FLT

[Kevin Buzzard]

I have made a big push on the Haar character project over the last few days. The relevant chapter of the blueprint now has details of all the more subtle arguments (or more precisely will have when the just-merged FLT#502 finishes CI), and there are formalized Lean statements of everything up to and including section 9.6 (finite products); over the next couple of days I should make it to the end.

I have just opened 14 new tasks; you can see them here. They range from straightforward to "you should know something about the integration API to do this one". Recall that you can see a list of unclaimed tasks here and instructions on how to claim a task are here.

If you're interested in seeing the Lean statement of the task explained in issue FLT#xyz then just search for FLT#xyz in the Lean files of the project.

@Edison Xie you asked if you could do FLT#518 after exams -- now is your chance to claim it.

I've tagged 6 of the tasks with "straightforward" -- this is stuff which I think one could just sit down and do in one sitting. If I've got this hopelessly wrong then let me know and I'll remove the tag!

[Kevin Buzzard]

Hmm, I think I am going to embark on a refactor of the definition of mulEquivHaarChar to use maps instead of comaps based on the discussions I've had with Gouezel and Degenne recently, so anyone considering claiming one of these things, beware! There is a lot more API for maps than comaps so this will make life easier.

[Ruben Van de Velde]

I'd been poking at it with little success, so I hope it'll help :)

[Kevin Buzzard]

I had not understood properly when I wrote the plan that measure theorists don't like pullbacks of measures because the natural definition $\phi^*\mu(X)=\mu(\phi(X))$ is problematic sometimes, as the image of a measurable set might not be measurable (even for nice maps like the projection $\R^2\to\R$); the definition of a measurable function is that preimage of measurable is measurable. So there's far more API for pushforwards of measures, defined by $\phi_*\mu(X)=\mu(\phi^{-1}(X)).$

[Kevin Buzzard]

For example I needed "the comap of a regular Borel measure along a homeomorphism is regular" which isn't there, but the lemma is there for maps. I just spent over an hour writing a proof that the comap of $c\mu$ is $c$ times the comap but this is there for maps etc etc.

[Sébastien Gouëzel]

It's not so much that we don't like pullbacks, it's that some objects you can naturally pullback, and some objects you can naturally pushforward. I'm sure you have plenty of examples in algebraic geometry.

[Kevin Buzzard]

OK, it's great to see what's happening here; I opened something like 14 tasks a few days ago and there are only three unclaimed. Thanks to everyone who has been involved. I am now opening 6 more; the Haar character blueprint is now completely wired up to Lean apart from the last section, which I'm about to start working on; this may well throw up some more tasks.

Just to give an overview of the new tasks which have just appeared on the project dashboard: they are mostly related to restricted products. If $A_i$ are types each equipped with a subset $C_i$ then the docs#RestrictedProduct of this data $\prod'_i A_i$ is the subset of $\prod_i A_i$ consisting of $(a_i)$ such that $a_i\in C_i$ for all but finitely many $i$. If the $A_i$ are groups and the $C_i$ are subgroups then the restricted product is a group; if the $A_i$ are topological groups and the $C_i$ are open subgroups then the restricted product is a topological group (although the topology is not the subspace topology of the product topology; see mathlib's restricted product file for the definition). The new sorries are listed below. A cheap way to find the Lean sorry is just to search the Lean files in the repo for the issue number.

1) The sorries required to show that maps on factors $A_i\to A_i'$ induce a map on restricted products (I defined all the data, filling the proof fields should be straightforward). This is FLT#530

2) FLT#531: if the $A_i$ are topological spaces and we have another collection of topological spaces $A'_i$ equpped with subsets $C_i'$ then a collection of continuous maps $A_i\to A_i'$ sending $C_i$ to $C_i'$ for almost all $i$ induces a continuous function $\prod'_i A_i\to\prod'_i A_i'$$ (proof uses the universal property which Anatole already proved in mathlib).

3) FLT#551: this has nothing to do with restricted products; it's just the claim that the Haar measure fudge factor coming from a homeomorphism+group automorphism of a locally compact group can be computed on an open subgroup which is fixed (as a set) by the automorphism. We need it for a later calculation. The proof is in the blueprint and hopefully I've made all the prerequisites so this might be straightforward.

4) If we have homeomorphisms + group automorphisms of locally compact groups $A_i$ all but finitely many of which fix compact open subgroups $C_i$ then the Haar fudge factor of the induced ContinuousMulEquiv of the restricted product is the product of the local fudge factors. I sketch a proof in the blueprint. This is probably the most challenging of the new sorrys.

5) The units of a restricted product of monoids wrt submonoids is naturally isomorphic to the restricted product of the units of the monoid wrt the units of the submonoid. I've filled in all the data, there are 10 sorries and they should all be easy. This is #553.

6) Haar character of a unit in a restricted product of locally compact topological rings wrt compact open subrings is equal to the product of the Haar characters of the factors. This hopefully is really easy now, assuming all the machinery above, so I marked it straightforward. It's #554.

Thanks everyone for all their help so far!

[Anatole Dedecker]

Very minor note: I have a shorter proof of the recently merged Continuous.restrictedProduct_map at #24915 (arguably I didn't advertise it at all and I should have made a PR to FLT instead). The core of the argument is the same of course.

[Kevin Buzzard]

Thanks a lot! I hadn't seen this PR; I have a big talk at Big Proof in two weeks and I've been ignoring github notifications and just spending all my Lean time on FLT recently. Making PRs to mathlib is far preferable to making PRs to FLT, a lot of the restricted product stuff we're making should be upstreamed in the end and the best way to do this is to just never put it into FLT in the first place. We are bumping mathlib weekly, on average, so will just adapt when it appears in FLT.