descending measures to compact quotients

Stream: Is there code for X?

[Kevin Buzzard]

I don't know my way around the measure theory part of the library at all, but I need a compactness result which I think I'm going to prove using measure theory.

The set-up is: $A$ is a (locally compact, second countable) additive abelian topological group, $D\subseteq A$ is a discrete (closed) subgroup, and I know the quotient $A/D$ is compact. I want to prove the existence of a compact subset $E\subseteq A$ such that the composite $E\to A\to A/D$ is not injective. If we put Haar measure on $A$ then I am able to construct compact subsets of $A$ with arbitrarily large measure, so my plan is to say that $A/D$ is compact so has finite measure $M$ if we give it the quotient measure, I choose compact $E\subseteq A$ with measure larger than $M$ and then I say that by measure-theory magic the induced map $E\to A/D$ can't be injective. I would imagine that in our work on Minkowski bounds for class groups we must have already done something like this in the case $A=\R^n$; I have some adelic $A$ but I'm hoping that the (perhaps vague?) argument above is still rigorous (my understanding of measure theory is entirely vibes-based). Do we have all the required machinery (if it even exists?)

[Aaron Liu]

Is $D$ the subgroup or is $A$ the subgroup?

[Kevin Buzzard]

Sorry! "both" was the answer with the initial version of the post but hopefully I've got everything straight now.

[Aaron Liu]

Let $A$ be the trivial group, which is a locally compact second countable topological group, and let $D$ be its unique subgroup, which is discrete and closed. The quotient $A / D$ is again the trivial group, which is compact. Then $E \subseteq A$ must be a subsingleton and so all maps out of $E$ are injective.

[Kevin Buzzard]

Yes but in my situation I also have the hypothesis that for all positive real $M$ I can find a compact $E\subseteq A$ with Haar measure greater than $M$. Sorry for not being clearer.

[Aaron Liu]

Suppose $A$ is compact. Then the Haar measure is bounded, contradicting your hypothesis. So $A$ is not compact. Since $A$ is noncompact but $A / D$ is compact, $D$ must be nontrivial. Choose two distinct elements $a, b \in D$, and set $E = \{a, b\}$, which is finite and therefore compact. Now since $E \subseteq D$, we have that $E \to A \to A / D$ is zero, which is not injective since $E$ is nontrivial.

[Andrew Yang]

I think Kevin has simplified the question too much. $A$ is actually a ring in the application, and we need $E \subseteq A$ such that $xE \to A \to A/D$ is injective for all invertible $x$.

[Kevin Buzzard]

Yeah that's no good for my application either, but your examples are helping me to formulate the question correctly. I think what I need is the existence of some positive real $M$ such that if $E$ is any Borel set with measure > $M$ then $E\to A\to A/D$ is not injective, and my proposal is to hope that there's something called a quotient measure, then measure $A/D$ with it and get $M$, and then hope that this $M$ works.

[Kevin Buzzard]

Andrew has gone too far, I only need it for $x$ such that left multiplication by $x$ doesn't change the measure, so that's why I can stick to asking for $M$.

[Sébastien Gouëzel]

We have docs#MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd, which has the same flavor as what you're asking.

[Kevin Buzzard]

Hmm. But do I now have to find a fundamental domain? I don't have one to hand in the application, all I know is that the quotient is compact

[Kevin Buzzard]

(The subgroup is countable so this is ok)

[Yaël Dillies]

You should be able to make a fundamental domain in $A$ which is mapped bijectively to $A / D$ under the quotient map, except on some null set

[Kevin Buzzard]

How?

[Kevin Buzzard]

A has no sensible metric or norm and has no good group-theoretic properties

[Kevin Buzzard]

I feel like this is the wrong approach -- probably one should understand the proof in mathlib and adapt it to deal with my situation somehow

[Aaron Liu]

I think you can define a sort of "quotient measure" and do stuff with that

[Kevin Buzzard]

Right that's my gut feeling, and my question is whether this machinery is in mathlib. I have no idea how to make the fundamental domain -- I have seen quite a general machine for making fundamental domains but this is in symmetric spaces like $\R^n$ or the upper half plane with a discrete action of a group, and the distance function played a crucial role. Here the space is adelic and it would be a pain to reduce to a situation with a distance function.

[Sébastien Gouëzel]

Is the quotient map locally a homeo? If so, you can build easily a (measurable) fundamental domain as follows. For each point x downstairs, choose an open set U_x around x, which is the homeomorphic image of an open set V_x upstairs by the projection. Let U_1, ..., U_n be a finite subcover. Let U'_i = U_i \ (U_1 \cup ... \cup U_{i-1}): the U'_i form a partition of the base space by measurable subsets, which can each be lifted upstairs, to a set V'_i = V_i \cap \pi^{-1} U'_i. Then the union of the V'_i is a fundamental domain upstairs.

[Kevin Buzzard]

Is the quotient map locally a homeo?

Yes, I had guessed that this was more than necessary (e.g. I could imagine quotienting out $\R\times S^1$ by $\R$) but in my case I have a discrete subgroup and I'm quotienting out by it. Yes hopefully this construction will do it, thanks!

[Antoine Chambert-Loir]

How do you know that your quotient group is compact? In the cases I know, the quotient is proved to be compact by exhibiting a set of bounded measure that maps surjectively.

[Kevin Buzzard]

In my case I prove $\prod_p\Z_p\times[0,1]$ surjects onto $\mathbb{A}_{\mathbb{Q}}/\mathbb{Q}$ so $\mathbb{A}_{\mathbb{Q}}/\mathbb{Q}$ is compact, and then for general number field $K$ I deduce that $\mathbb{A}_K/K$ is compact by proving that $\mathbb{A}_K=K\otimes\mathbb{A}_{\mathbb{Q}}$. I guess you're right in that if I choose a basis I could get a fundamental domain but then I would have to work to show that $\prod_p\Z_p\times[0,1]$ is a fundamental domain for $\mathbb{Q}$ (and to pick a basis of $K$) and mathematically I don't need to do that.

[Antoine Chambert-Loir]

Then i'm afraid you have no other option than the one suggested by Sébastien, which, for group quotients, is more or less an iff.

[Antoine Chambert-Loir]

Do we have the existence of Borel sections?

[Sébastien Gouëzel]

I don't think we have Borel sections. But doesn't this require assumptions such as Polish (which are not satisfied in Kevin's generality)? -- although I'm sure Kevin would be happy with second-countability assumptions, because he's only interested in concrete applications.

[Antoine Chambert-Loir]

Yes, and that doesn't help anyway, because the closure of the image of the Borel section could be non compact.

[Antoine Chambert-Loir]

Given what you have done for the change of variables formula, I'd guess that Borel sections are not far.

[Antoine Chambert-Loir]

Returning to Kevin's question, I believe that it is mathematically better to get the compact fundamental domain (I mean, compact and surjecting to the quotient) using the tensor product form and the existence of such a domain for $\mathbf Q$ than going in 3 steps (compactness of quotient for $\mathbf Q$, compactness of quotient for $K$, existence of a domain for $K$).

[Kevin Buzzard]

I just feel a little cheated here because I don't see why I need to put in the extra work to go from "this compact set surjects onto $A/D$" (which is mathematically enough for my application and which I already have) to "this compact set is a fundamental domain" which will need a little more effort. The mathematical advantage that the work gives me is that I can get the stronger output "for this explicit real number X, any measurable subset of A with measure bigger than X doesn't inject into $A/D$", but all I want is the weaker statement "there exists some real number X such that ...".

[Sébastien Gouëzel]

Antoine Chambert-Loir said:

Given what you have done for the change of variables formula, I'd guess that Borel sections are not far.

Yes, Borel sections are quite easy in fact.