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.