ContinuousMulEquiv.isHaarMeasure_map

Stream: mathlib4

[Kevin Buzzard]

I'm very excited to see docs#ContinuousMulEquiv (homeomorphisms which are group isomorphisms) merged and now want to start using it by pushing Haar measures along such things.

Right now we have docs#MeasureTheory.Measure.isHaarMeasure_map which works for group homomorphisms f satisfying a bunch of annoying-to-fill-in properties like Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H), and then we have what mathlib calls a "convenience wrapper", docs#MulEquiv.isHaarMeasure_map, which asks for fewer annoying properties but still wants (e : G ≃* H) (he : Continuous ⇑e) (hesymm : Continuous ⇑e.symm), which is exactly what a ContinuousMulEquiv is. We also have another convenience wrapper docs#ContinuousLinearEquiv.isAddHaarMeasure_map (a linear map version), which makes me think that we will not be averse to this declaration:

import Mathlib

/--
Yet another convenience wrapper for MeasureTheory.Measure.isHaarMeasure_map.
-/
@[to_additive "Yet another convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map.
"]
lemma ContinuousMulEquiv.isHaarMeasure_map {G : Type*} [MeasurableSpace G] [Group G]
    [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G]
    [TopologicalGroup G] {H : Type*} [Group H] [TopologicalSpace H] [MeasurableSpace H]
    [BorelSpace H] [TopologicalGroup H] (e : G ≃ₜ* H) :
    (MeasureTheory.Measure.map (⇑e) μ).IsHaarMeasure :=
  e.toMulEquiv.isHaarMeasure_map μ e.continuous e.symm.continuous

My first question is: do we in fact want this? My (dependent) second question is: if we do, it can't go in Mathlib.MeasureTheory.Group.Measure with the other wrappers as it stands because this file doesn't import Mathlib.Topology.Algebra.ContinuousMonoidHom where ≃ₜ* is defined (even though ContinuousLinearEquiv is imported!). Can I add this import? I don't know my way around this part of mathlib at all.

[Sébastien Gouëzel]

We definitely want to do this, and you can add the import (it's pretty low-level compared to Haar measures, so this is completely reasonable).

[Kevin Buzzard]

Thanks! In fact later on it occurred to me that it was quite funny that the file imports continuous module isomorphisms but not continuous additive group isomorphisms.

[Kevin Buzzard]

#20469

[Eric Wieser]

I've since created #21443 which lessens the weight of the ContinousMonoidHom import