|
| 1 | +/- |
| 2 | +Copyright (c) 2022 Alex Kontorovich and Heather Macbeth. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Alex Kontorovich, Heather Macbeth |
| 5 | +-/ |
| 6 | + |
| 7 | +import measure_theory.measure.haar |
| 8 | +import measure_theory.group.fundamental_domain |
| 9 | +import topology.compact_open |
| 10 | +import algebra.group.opposite |
| 11 | + |
| 12 | +/-! |
| 13 | +# Haar quotient measure |
| 14 | +
|
| 15 | +In this file, we consider properties of fundamental domains and measures for the action of a |
| 16 | +subgroup of a group `G` on `G` itself. |
| 17 | +
|
| 18 | +## Main results |
| 19 | +
|
| 20 | +* `measure_theory.is_fundamental_domain.smul_invariant_measure_map `: given a subgroup `Γ` of a |
| 21 | + topological group `G`, the pushforward to the coset space `G ⧸ Γ` of the restriction of a both |
| 22 | + left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a `G`-invariant measure |
| 23 | + on `G ⧸ Γ`. |
| 24 | +
|
| 25 | +* `measure_theory.is_fundamental_domain.is_mul_left_invariant_map `: given a normal subgroup `Γ` of |
| 26 | + a topological group `G`, the pushforward to the quotient group `G ⧸ Γ` of the restriction of |
| 27 | + a both left- and right-invariant measure on `G` to a fundamental domain `𝓕` is a left-invariant |
| 28 | + measure on `G ⧸ Γ`. |
| 29 | +
|
| 30 | +Note that a group `G` with Haar measure that is both left and right invariant is called |
| 31 | +**unimodular**. |
| 32 | +-/ |
| 33 | + |
| 34 | +open set measure_theory topological_space measure_theory.measure |
| 35 | + |
| 36 | +variables {G : Type*} [group G] [measurable_space G] [topological_space G] |
| 37 | + [topological_group G] [borel_space G] |
| 38 | + {μ : measure G} |
| 39 | + {Γ : subgroup G} |
| 40 | + |
| 41 | +/-- Given a subgroup `Γ` of `G` and a right invariant measure `μ` on `G`, the measure is also |
| 42 | + invariant under the action of `Γ` on `G` by **right** multiplication. -/ |
| 43 | +@[to_additive "Given a subgroup `Γ` of an additive group `G` and a right invariant measure `μ` on |
| 44 | + `G`, the measure is also invariant under the action of `Γ` on `G` by **right** addition."] |
| 45 | +lemma subgroup.smul_invariant_measure [μ.is_mul_right_invariant] : |
| 46 | + smul_invariant_measure Γ.opposite G μ := |
| 47 | +{ measure_preimage_smul := |
| 48 | +begin |
| 49 | + rintros ⟨c, hc⟩ s hs, |
| 50 | + dsimp [(•)], |
| 51 | + refine measure_preimage_mul_right μ (mul_opposite.unop c) s, |
| 52 | +end} |
| 53 | + |
| 54 | +/-- Measurability of the action of the topological group `G` on the left-coset space `G/Γ`. -/ |
| 55 | +@[to_additive "Measurability of the action of the additive topological group `G` on the left-coset |
| 56 | + space `G/Γ`."] |
| 57 | +instance quotient_group.has_measurable_smul [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] : |
| 58 | + has_measurable_smul G (G ⧸ Γ) := |
| 59 | +{ measurable_const_smul := λ g, (continuous_const_smul g).measurable, |
| 60 | + measurable_smul_const := λ x, (quotient_group.continuous_smul₁ x).measurable } |
| 61 | + |
| 62 | +variables {𝓕 : set G} (h𝓕 : is_fundamental_domain Γ.opposite 𝓕 μ) |
| 63 | +include h𝓕 |
| 64 | + |
| 65 | +/-- If `𝓕` is a fundamental domain for the action by right multiplication of a subgroup `Γ` of a |
| 66 | + topological group `G`, then its left-translate by an element of `g` is also a fundamental |
| 67 | + domain. -/ |
| 68 | +@[to_additive "If `𝓕` is a fundamental domain for the action by right addition of a subgroup `Γ` |
| 69 | + of an additive topological group `G`, then its left-translate by an element of `g` is also a |
| 70 | + fundamental domain."] |
| 71 | +lemma measure_theory.is_fundamental_domain.smul (g : G) [μ.is_mul_left_invariant] : |
| 72 | + is_fundamental_domain ↥Γ.opposite (has_mul.mul g ⁻¹' 𝓕) μ := |
| 73 | +{ measurable_set := measurable_set_preimage (measurable_const_mul g) (h𝓕.measurable_set), |
| 74 | + ae_covers := begin |
| 75 | + let s := {x : G | ¬∃ (γ : ↥(Γ.opposite)), γ • x ∈ 𝓕}, |
| 76 | + have μs_eq_zero : μ s = 0 := h𝓕.2, |
| 77 | + change μ {x : G | ¬∃ (γ : ↥(Γ.opposite)), g * γ • x ∈ 𝓕} = 0, |
| 78 | + have : {x : G | ¬∃ (γ : ↥(Γ.opposite)), g * γ • x ∈ 𝓕} = has_mul.mul g ⁻¹' s, |
| 79 | + { ext, |
| 80 | + simp [s, subgroup.smul_opposite_mul], }, |
| 81 | + rw [this, measure_preimage_mul μ g s, μs_eq_zero], |
| 82 | + end, |
| 83 | + ae_disjoint := begin |
| 84 | + intros γ γ_ne_one, |
| 85 | + have μs_eq_zero : μ (((λ x, γ • x) '' 𝓕) ∩ 𝓕) = 0 := h𝓕.3 γ γ_ne_one, |
| 86 | + change μ (((λ x, γ • x) '' (has_mul.mul g ⁻¹' 𝓕)) ∩ (has_mul.mul g ⁻¹' 𝓕)) = 0, |
| 87 | + rw [subgroup.smul_opposite_image_mul_preimage, ← preimage_inter, measure_preimage_mul μ g _, |
| 88 | + μs_eq_zero], |
| 89 | + end } |
| 90 | + |
| 91 | +variables [encodable Γ] [measurable_space (G ⧸ Γ)] [borel_space (G ⧸ Γ)] |
| 92 | + |
| 93 | +/-- The pushforward to the coset space `G ⧸ Γ` of the restriction of a both left- and right- |
| 94 | + invariant measure on `G` to a fundamental domain `𝓕` is a `G`-invariant measure on `G ⧸ Γ`. -/ |
| 95 | +@[to_additive "The pushforward to the coset space `G ⧸ Γ` of the restriction of a both left- and |
| 96 | + right-invariant measure on an additive topological group `G` to a fundamental domain `𝓕` is a |
| 97 | + `G`-invariant measure on `G ⧸ Γ`."] |
| 98 | +lemma measure_theory.is_fundamental_domain.smul_invariant_measure_map |
| 99 | + [μ.is_mul_left_invariant] [μ.is_mul_right_invariant] : |
| 100 | + smul_invariant_measure G (G ⧸ Γ) (measure.map quotient_group.mk (μ.restrict 𝓕)) := |
| 101 | +{ measure_preimage_smul := |
| 102 | + begin |
| 103 | + let π : G → G ⧸ Γ := quotient_group.mk, |
| 104 | + have meas_π : measurable π := |
| 105 | + continuous_quotient_mk.measurable, |
| 106 | + have 𝓕meas : measurable_set 𝓕 := h𝓕.measurable_set, |
| 107 | + intros g A hA, |
| 108 | + have meas_πA : measurable_set (π ⁻¹' A) := measurable_set_preimage meas_π hA, |
| 109 | + rw [measure.map_apply meas_π hA, |
| 110 | + measure.map_apply meas_π (measurable_set_preimage (measurable_const_smul g) hA), |
| 111 | + measure.restrict_apply' 𝓕meas, measure.restrict_apply' 𝓕meas], |
| 112 | + set π_preA := π ⁻¹' A, |
| 113 | + have : (quotient_group.mk ⁻¹' ((λ (x : G ⧸ Γ), g • x) ⁻¹' A)) = has_mul.mul g ⁻¹' π_preA, |
| 114 | + { ext1, simp }, |
| 115 | + rw this, |
| 116 | + have : μ (has_mul.mul g ⁻¹' π_preA ∩ 𝓕) = μ (π_preA ∩ has_mul.mul (g⁻¹) ⁻¹' 𝓕), |
| 117 | + { transitivity μ (has_mul.mul g ⁻¹' (π_preA ∩ has_mul.mul g⁻¹ ⁻¹' 𝓕)), |
| 118 | + { rw preimage_inter, |
| 119 | + congr, |
| 120 | + rw [← preimage_comp, comp_mul_left, mul_left_inv], |
| 121 | + ext, |
| 122 | + simp, }, |
| 123 | + rw measure_preimage_mul, }, |
| 124 | + rw this, |
| 125 | + have h𝓕_translate_fundom : is_fundamental_domain Γ.opposite (has_mul.mul g⁻¹ ⁻¹' 𝓕) μ := |
| 126 | + h𝓕.smul (g⁻¹), |
| 127 | + haveI : smul_invariant_measure ↥(Γ.opposite) G μ := subgroup.smul_invariant_measure, |
| 128 | + rw h𝓕.measure_set_eq h𝓕_translate_fundom meas_πA, |
| 129 | + rintros ⟨γ, γ_in_Γ⟩, |
| 130 | + ext, |
| 131 | + have : π (x * (mul_opposite.unop γ)) = π (x) := by simpa [quotient_group.eq'] using γ_in_Γ, |
| 132 | + simp [(•), this], |
| 133 | + end } |
| 134 | + |
| 135 | +/-- Assuming `Γ` is a normal subgroup of a topological group `G`, the pushforward to the quotient |
| 136 | + group `G ⧸ Γ` of the restriction of a both left- and right-invariant measure on `G` to a |
| 137 | + fundamental domain `𝓕` is a left-invariant measure on `G ⧸ Γ`. -/ |
| 138 | +@[to_additive "Assuming `Γ` is a normal subgroup of an additive topological group `G`, the |
| 139 | + pushforward to the quotient group `G ⧸ Γ` of the restriction of a both left- and right-invariant |
| 140 | + measure on `G` to a fundamental domain `𝓕` is a left-invariant measure on `G ⧸ Γ`."] |
| 141 | +lemma measure_theory.is_fundamental_domain.is_mul_left_invariant_map [subgroup.normal Γ] |
| 142 | + [μ.is_mul_left_invariant] [μ.is_mul_right_invariant] : |
| 143 | + (measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)).is_mul_left_invariant := |
| 144 | +{ map_mul_left_eq_self := begin |
| 145 | + intros x, |
| 146 | + apply measure.ext, |
| 147 | + intros A hA, |
| 148 | + obtain ⟨x₁, _⟩ := @quotient.exists_rep _ (quotient_group.left_rel Γ) x, |
| 149 | + haveI := h𝓕.smul_invariant_measure_map, |
| 150 | + convert measure_preimage_smul x₁ ((measure.map quotient_group.mk) (μ.restrict 𝓕)) A using 1, |
| 151 | + rw [← h, measure.map_apply], |
| 152 | + { refl, }, |
| 153 | + { exact measurable_const_mul _, }, |
| 154 | + { exact hA, }, |
| 155 | + end } |
| 156 | + |
| 157 | +variables [t2_space (G ⧸ Γ)] [second_countable_topology (G ⧸ Γ)] (K : positive_compacts (G ⧸ Γ)) |
| 158 | + |
| 159 | +/-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also |
| 160 | + right-invariant, and a finite volume fundamental domain `𝓕`, the pushforward to the quotient |
| 161 | + group `G ⧸ Γ` of the restriction of `μ` to `𝓕` is a multiple of Haar measure on `G ⧸ Γ`. -/ |
| 162 | +@[to_additive "Given a normal subgroup `Γ` of an additive topological group `G` with Haar measure |
| 163 | + `μ`, which is also right-invariant, and a finite volume fundamental domain `𝓕`, the pushforward |
| 164 | + to the quotient group `G ⧸ Γ` of the restriction of `μ` to `𝓕` is a multiple of Haar measure on |
| 165 | + `G ⧸ Γ`."] |
| 166 | +lemma measure_theory.is_fundamental_domain.map_restrict_quotient [subgroup.normal Γ] |
| 167 | + [measure_theory.measure.is_haar_measure μ] [μ.is_mul_right_invariant] |
| 168 | + (h𝓕_finite : μ 𝓕 < ⊤) : measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕) |
| 169 | + = (μ (𝓕 ∩ (quotient_group.mk' Γ) ⁻¹' K.val)) • (measure_theory.measure.haar_measure K) := |
| 170 | +begin |
| 171 | + let π : G →* G ⧸ Γ := quotient_group.mk' Γ, |
| 172 | + have meas_π : measurable π := continuous_quotient_mk.measurable, |
| 173 | + have 𝓕meas : measurable_set 𝓕 := h𝓕.measurable_set, |
| 174 | + haveI : is_finite_measure (μ.restrict 𝓕) := |
| 175 | + ⟨by { rw [measure.restrict_apply' 𝓕meas, univ_inter], exact h𝓕_finite }⟩, |
| 176 | + -- the measure is left-invariant, so by the uniqueness of Haar measure it's enough to show that |
| 177 | + -- it has the stated size on the reference compact set `K`. |
| 178 | + haveI : (measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)).is_mul_left_invariant := |
| 179 | + h𝓕.is_mul_left_invariant_map, |
| 180 | + rw [measure.haar_measure_unique (measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)) K, |
| 181 | + measure.map_apply meas_π, measure.restrict_apply' 𝓕meas, inter_comm], |
| 182 | + exact K.prop.1.measurable_set, |
| 183 | +end |
0 commit comments