Haar measures on affine spaces

Stream: maths

[Eric Wieser]

In #8511, I attempted to generalized Haar measures to work on affine spaces, but I quickly ran into a problem: docs#AddTorsor and vsub do not have a multiplicative analog that replaces vadd with smul, so while I think docs#compact_covered_by_add_left_translates generalizes nicely, docs#compact_covered_by_mul_left_translates does not.

[Eric Wieser]

I can see a few ways out of this:

• Add a multiplicative version of affine spaces
• Remove the multiplicative version of Haar measures
• Remove to_additive on all the haar measure machinery and replace them with manual AddTorsor versions

[Yaël Dillies]

We already talked about MulTorsor before. I think it's a good-ish idea?

[Eric Wieser]

Thanks for volunteering!

[Kevin Buzzard]

Haar measures on multiplicative groups (like $GL_n(\R)$) are used all over the Langlands program.

[Antoine Chambert-Loir]

As well as Haar measures on some homogeneous spaces under those.

[Eric Wieser]

It sounds pretty clear that MulTorsor (or just Torsor?) is the right choice then

[Eric Wieser]

Started in #8608