Some measure-theoretic preliminaries

LemmaTopology.IsOpenEmbedding.isHaarMeasure_comap #

Let \(A\) and \(B\) be locally compact topological groups and let \(f:A\to B\) be both a group homomorphism and open embedding. The pullback along \(f\) of a Haar measure on \(B\) is a Haar measure on \(A\).

Proof

Translation-invariance is easy, compact sets are finite because continuous image of compact is compact, open sets are bounded because image of open is open.

Lean

Formalized as Topology.IsOpenEmbedding.isHaarMeasure_comap.

Sources

Fermat's Last Theorem (Imperial) blueprint: chapter/HaarCharacterProject.tex, line 528

LeanTopology.IsOpenEmbedding.isHaarMeasure_comap

Discussionhttps://github.com/ImperialCollegeLondon/FLT/issues/507

Used by 1

Used byMeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding

LemmaTopology.IsOpenEmbedding.regular_comap #

The pullback of a regular Borel measure along an open embedding is a regular Borel measure.

Proof

Again this is because the image of compact is compact and the image of open is open, so all the properties of being a regular measure are easily checked.

Lean

Formalized as Topology.IsOpenEmbedding.regular_comap.

Sources

Fermat's Last Theorem (Imperial) blueprint: chapter/HaarCharacterProject.tex, line 543

LeanTopology.IsOpenEmbedding.regular_comap

Discussionhttps://github.com/ImperialCollegeLondon/FLT/issues/513

Used by 1

Used byMeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding

LemmaMeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace #

Say \(A\) is a compact topological additive group and \(\phi:A\to A\) is an additive isomorphism. Then \(d_A(\phi)=1.\)

Proof

We have \(d_A(\phi)\mu(A)=\mu(A)\) from lemma MeasureTheory.addEquivAddHaarChar_smul_preimage and \(\mu(A)\) is positive and finite because \(A\) is open and compact.

Lean

Formalized as MeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace.

Sources

Fermat's Last Theorem (Imperial) blueprint: chapter/HaarCharacterProject.tex, line 558

LeanMeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace

Discussionhttps://github.com/ImperialCollegeLondon/FLT/issues/532

LemmaMeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding #

If \(f:A\to B\) is a group homomorphism and open embedding between locally compact topological additive groups and if \(\alpha:A\to A\) and \(\beta:B\to B\) are additive homeomorphisms such that the square commutes (i.e., \(f\circ\alpha=\beta\circ f\)) then \(d_A(\alpha)=d_B(\beta)\).

Proof

Choose a regular Haar measure \(\mu_B\) on \(B\). We just saw in lemmas Topology.IsOpenEmbedding.isHaarMeasure_comap and Topology.IsOpenEmbedding.regular_comap that its pullback \(\mu_A:=f^*\mu_B\) to \(A\) is also a regular Haar measure. Now fix a continuous compactly-supported function \(g\) on \(A\) with \(0\lt \int g(a)d\mu(a)\lt \infty\). Then \(d_A(\alpha)\int g(a)d\mu_A(a)=\int g(a)d(\alpha^*\mu_A)(a)\) by lemma MeasureTheory.addEquivAddHaarChar_smul_integral_comap. This equals \(\int g(a)d(\alpha^* f^*\mu_B)(a)\) by definition, which is \(\int g(a)d(f^*\beta^*\mu_B)(a)\) because pullback of pullback is pullback. This equals \(d_B(\beta)\int g(a) d(f^*\mu_B)(a)\) by corollary MeasureTheory.addEquivAddHaarChar_comap which is \(d_B(\beta)\int g(a)d\mu_A(a)\) by definition, and so \(d_A(\alpha)=d_B(\beta)\) as required.