invertible matrix scales volume by size of determinant

Stream: Is there code for X?

[Kevin Buzzard]

Let $R$ be some commutative ring equipped with an additive Haar measure $\mu$, and say $V=R^n$ is a finite free $R$-module. You can imagine that $R=\R$ or $\mathbb{C}$, but my actual use case is that $R$ is some ring of adeles. Equip $V$ with the product measure $\nu=``\mu^n"$, which will then be an additive Haar measure on $V$ (i.e. $\nu(X+v)=\nu(X)$. If $g\in GL_n(R)$ is an invertible matrix then multiplication by $g$ is an $R$-linear map $V\to V$, and pulling back $\nu$ along this map will give us another Haar measure, so it's equal to $\nu$ up to some scalar factor $d\in\R_{>0}$. Another way to get a positive real number out of this situation is to take the determinant of $g$ which is now in $R^\times$, and consider multiplication by $det(g)$ as an additive isomorphism $R\to R$, which hence will scale $R$'s Haar measure $\mu$ by some positive real number. I'm assuming that these two positive real numbers are related, and doing an example of a diagonal matrix makes me think that actually they're equal. Do we have anything like this in mathlib? It's some generalization of the claim that multiplication by an $n\times n$ real matrix on $\mathbb{R}^n$ scales volume by the absolute value of the determinant, and my instinct is that the proof in the more general case will basically be the same.

[Sébastien Gouëzel]

You have docs#MeasureTheory.Measure.addHaar_preimage_linearMap, and several versions around there.

[Floris van Doorn]

So we need to generalize $\mathbb{R}$ to $R$ in those lemmas?

[Sébastien Gouëzel]

Note that over other fields you get a power of the determinant. For instance, over the complex, it's the determinant squared. And you just need to check in one dimension to see which power it is.

[Andrew Yang]

A problem is that we do not have a norm $R \to \mathbb{R}$ in the setting so $\nu(gS) = \Vert\!\det(g)\Vert^{k}\nu(S)$ does not make sense. What is hopefully still true is that $\frac{\nu(gS)}{\nu(S)}$ (which does not depend on any positive measure set $S \subseteq V$) is equal to $\frac{\mu(\det(g) T)}{\mu(T)}$ (which also does not depend on $T \subseteq R$)

[Kevin Buzzard]

Sébastien Gouëzel said:

Note that over other fields you get a power of the determinant. For instance, over the complex, it's the determinant squared. And you just need to check in one dimension to see which power it is.

Yes, but I'm claiming that it's always the "norm" of the determinant, where "norm" is defined to be "factor by which Haar measure on the base is scaled". So for example multiplication by 3 scales Haar measure on $\mathbb{C}$ by a factor of $3^2$, so this factor is taken into account in my original claim.

[Sébastien Gouëzel]

Yes, that looks definitely true, and follows from the same proof as in the real case (check it for diagonal matrices, for transvections, and argue that these generate $GL_n$ -- at least in the field case, maybe there is some trickery with rings).

But note that you have a canonical norm, which is just the rescaling of the Haar measure in dimension 1. Except that over $\mathbb{C}$ it doesn't coincide with the usual norm, but with its square...

[Kevin Buzzard]

Yes, but the "usual norm" is not relevant here. There is a second "canonical norm", coming from the Haar measure, which is the square of the usual norm for $\mathbb{C}$, and which is the right factor. If you only ask "how much is Haar measure changed" (on the vector space and the field) then everything is equal on the nose.

[Kevin Buzzard]

For things like a field which is a finite degree $n$ extension of the $p$-adic numbers it's the same situation. There are two "canonical norms": one is "say how it changes the Haar measure" and the other is "ensure it agrees with the norm on $\mathbb{Q}_p$", and these differ by an $n$ th power. Here we don't care about making norms compatible when we change fields, because we never change base field, so I don't care that the canonical norm I'm putting on $\mathbb{C}$ does not agree with the norm that everyone is happy with on $\mathbb{R}$ under restriction, because I never restrict.

[Antoine Chambert-Loir]

Another approach is to use the result about norms and determinants that you discussed in another thread. Sébastien's proof is very good over a field, because one knows generators for the linear group. Then one can transfer it to general rings by the standard polynomial machinery.