Carneiro's thesis (transfer tactic not needed)

Stream: maths

[Kevin Buzzard]

Years ago Mario made the striking observation that in practice we didn't seem to need a tactic to prove that if X is homeomorphic to Y and if X is compact then Y is compact, because a more general mathematical statement was true: continuous image of compact is compact (and this is in mathlib), and you just apply this to the identity map. The discussion was about what we were missing out on by not having a univalence axiom and Mario's thesis was that this killer app (ability to transfer predicates along isomorphisms) was often not necessary (because they transferred over a more general class of maps, where univalence would not give you something for free) and we wanted the more general theorem in mathlib anyway, so could get the transfer theorem as a consequence.

I was skeptical about the thesis initially, and I even felt I had a counterexample: a local ring is a commutative ring with exactly 1 maximal ideal. How to prove that a ring isomorphic to a local ring is local? Eventually I managed to do it: say a ring is prelocal if it has at most 1 maximal ideal (so either a local ring or the zero ring). Then prelocal transfers along surjections, and "I am not the zero ring" transfers along injections, so local transfers along isomorphisms.

The one time I struggled to make the thesis apply was "something isomorphic to a unique factorization domain is a unique factorization domain" but I didn't try too hard to resolve this, I just proved it directly.

---

I've been developing some theory in FLT which has needed stuff about regular Haar measures on locally compact spaces, and I realised that I needed that Haar measure pulled back along topological isomorphisms to Haar measure, and regular measures pulled back along measure-theoretic isomorphisms to regular measures. Mathlib does indeed have docs#ContinuousMulEquiv.isHaarMeasure_map , and to my delight it was indeed proved using Carneiro's thesis: the pushforward of a Haar measure along a continuous proper surjective group homomorphism is a Haar measure.

Rather annoyingly though, in FLT I have set everything up with pullbacks (Measure.comap not Measure.map), so I'd still like to prove that the preimage of a Haar measure along an isomorphism is a Haar measure. I claim that this statement is true for open embeddings: if a group homomorphism $G\to H$ is an open embedding between locally compact topological groups then the pullback of a Haar measure on $H$ is a Haar measure on $G$; it's clearly translation-invariant, and open embeddings send opens to opens and compacts to compacts so I think I'm OK. Does this look good? My measure theory is shaky.

In FLT I also need that the property of a measure being regular pulls back under isomorphisms, and now I'm a bit less sure about what's going on because this is not a statement about topology. I suspect that again if $X\to Y$ is an open embedding and $\mu$ is a regular Borel measure on $Y$ then its pullback to $X$ is a regular Borel measure on $X$ but can we do any better? Is there some weaker statement than "I am a bijection inducing a bijection on sigma-algebras" for which regular measures push forward or pull back? It would be good enough to have distinct theorems about inner and outer regular I guess? But ideally we are pulling them back rather than pushing them forwards, unless we also have the theorem that the pushforward of a measure along a measurable iso is equal to the pullback...

[Sébastien Gouëzel]

In general the pullback of measures is not well defined, contrary to the push-forward: if you want to define $f_* \mu(s)$, you let it be $\mu(f^{-1} s)$, and if $f$ and $s$ are measurable then $f^{-1} s$ is measurable and you're fine. However, if you wanted to define $f^* \mu(s)$, you could try to define it as $\mu(f s)$, but even if $f$ and $s$ are measurable then $f s$ is not measurable, and you're in trouble.

[Sébastien Gouëzel]

(Even if $f$ is the first projection from $\R^2$ to $\R$: this map sends open sets to open sets, compact sets to compact sets, and still it doesn't send measurable sets to measurable sets)

[Kevin Buzzard]

Oh interesting! So this is why you prefer pushforwards? You know exactly why I am doing this -- I want to compare Haar measure on a locally compact topological ring before and after multiplication by a unit, but in general pullbacks in algebraalgebraic geometry are better-behaved than pushforwards (e.g. pullback of a free module along an arbitrary ring homomorphism is free)(e.g. pullback of a vector bundle is a vector bundle, pushforward of a vector bundle is a mess) so my instinct is always to use pullback even if we're working with an isomorphism. Do we have that pullback of a Borel measure along a homeo equals pushforward of the measure along the inverse homeo? That would be a cheap escape for me.

I would imagine that pullbacks along open embeddings are rather better behaved, of course :-) (at least for Borel measures) and today I convinced myself that I really needed this. To get technical, consider the finite adeles of $\mathbb{Q}$, defined algebraically as the subring of $\prod_p\mathbb{Q}_p$ consisting of elements which are in $\Z_p$ for all but finitely many $p$. This can be topologised by letting $\prod_p\Z_p$ be open with the product topology (note that $\Z_p$ is compact and open in $\mathbb{Q}_p$ but $\prod_p\Z_p$ is not open in $\prod_p\mathbb{Q}_p$ so the finite adeles don't get the subspace topology; Anatole has written down the correct topology in mathlib, you take a colimit of $\prod_{p\in S}\mathbb{Q}_p\times\prod_{p\not\in S}\Z_p$ as $S$ varies over finite sets of primes and you give these the product topology). I claim that if $a$ is a unit in this ring and $\delta(a)$ denotes the factor by which multiplication by $a$ scales Haar measure then $\delta(a)=\prod_p\delta_{\mathbb{Q}_p}(a_p)$ and the product is finite. To prove this I want to prove it for $\prod_{p\in S}\mathbb{Q}_p\times\prod_{p\not\in S}\Z_p$ where $S$ is the finite set of primes for which $a_p\not\in\Z_p^\times$ and then I want to use the fact, proved by Anatole, that the inclusion from that into the finite adeles is an open embedding.

To make all this work I propose proving that if $\phi:G\cong G$ is an algebraic and topological isomorphism from a locally compact additive abelian group to itself, and $\psi:H\to H$ is another one (in the application these are multiplication by $a$), and if $G\to H$ is an open embedding and a group homomorphism, then $\phi$ and $\psi$ change their respective Haar measures by the same factor. Hmm. I wanted to argue that pulling back measures was a natural thing to do here as I can pull back Haar measure on $H$ to $G$ and now I have an extremely convenient relation between the two, namely that things in $G$ have the same measure whether you measure them in $G$ or $H$. Pushing forward a Haar measure along an inclusion won't give you a Haar measure in general so I might be stuck with pullbacks (unless I just work with unrelated Haar measures on source and target which just seems to add extra work).

[Etienne Marion]

Kevin Buzzard said:

Do we have that pullback of a Borel measure along a homeo equals pushforward of the measure along the inverse homeo?

It's docs#MeasurableEquiv.map_symm.

[Etienne Marion]

Probably along with docs#Homeomorph.toMeasurableEquiv.

[Sébastien Gouëzel]

Along open embeddings, everything is fine, of course! They're just inclusions, and restricting a measure to a subset is something we do all the time. The bad news is that, since it's a pretty bad notion in general, there will be very little API for it, and you will need to develop it. I just asked loogle about docs#MeasureTheory.Measure.comap, and there are only 57 hits, none of them mentioning regularity classes for instance. However, you don't really need regularity to discuss what you want to do: to compute the Haar scalar factor, one compares the ratio of integrals of some (any!) test function which is compactly supported, nonnegative and nonzero. Use such a function which is contained in your subgroup (or more generally in the image of your open embedding), and it follows readily that the Haar scalar factors are the same.

[Kevin Buzzard]

Right -- I was going to do the same with a compact neighbourhood of {1} in the smaller group (although I know you prefer to work with functions)

[Kevin Buzzard]

Do we have "in a locally compact space there's a compactly-supported nonzero nonnegative function"?

[Etienne Marion]

I guess you want some regularity? There is docs#exists_continuous_nonneg_pos.

[Sébastien Gouëzel]

Or docs#exists_continuous_one_zero_of_isCompact if you want to control the set where the function is nonzero.

[Kevin Buzzard]

Thanks! I think I still need to pull back (or push forward) regularity of a borel measure along an isomorphism though, at least if I want to avoid second countability assumptions.

[Etienne Marion]

MeasureTheory.Measure.Regular.map?

[Kevin Buzzard]

Yes I see now, I looked for it for comaps but it's only now I understand that you prefer maps! And this is a counterexample to Carneiro's thesis? You don't deduce the result from some more general theorem saying that pushforward of a Borel measure along a more general map is a Borel measure? So this mathlib theorem should be generated by the transfer tactic?

[Michael Rothgang]

What about InnerRegular.map_oft_continuous?

[Michael Rothgang]

That's what you use to prove Regular.map, if I saw correctly

[Kevin Buzzard]

So docs#MeasureTheory.Measure.InnerRegular.map_of_continuous proves that inner Borel regular maps push forward along continuous functions, so to demonstrate the thesis in this case one will need to push outer Borel regular maps forward along a (possibly different class of) function (and the class must include homeomorphisms as a special case)