10. Miniproject: Haar Characters
10.1. Goal
The goal of this miniproject is to develop the theory, that is, the basic API,
of Haar characters. Haar character is a name I've made up to describe a
certain character of the units of a locally compact topological ring. The main
result we need here is that if B is a finite-dimensional algebra over a
number field K, then B^\times is in the kernel of the Haar character of
B\otimes_K\A_K, where \A_K is the ring of adeles of K. Most if not all
of this should probably be in mathlib.
KMB would like to heartily thank Sebastien Gouezel for the help he gave during the preparation of this material.
10.2. Initial definitions
10.2.1. Scaling Haar Measure On A Group
Let A be a locally compact topological additive abelian group. There's then
a regular additive Haar measure \mu on A, unique up to a positive
scalar factor. If φ : (A, +) ≃ (A, +) is a homeomorphism and an additive
automorphism of A, then we can push forward μ along φ to get a second
measure φ_* μ on A, with the property that
(φ_* μ)(X) = μ(φ^{-1} X) for any Borel subset X of A.
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.addEquivAddHaarChar[complete]
If A is a locally compact topological additive abelian group, if \mu is a
regular Haar measure on A, and if \phi:A\to A is an additive
homeomorphism, then we let d_A(\phi) denote the unique positive real number
such that \mu(X)=d_A(\phi)(\phi_*\mu)(X) for any Borel set X.
Lean code for Definition10.2.1.1●1 definition
Associated Lean declarations
-
MeasureTheory.addEquivAddHaarChar[complete]
-
MeasureTheory.addEquivAddHaarChar[complete]
-
defdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
def MeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNReal
def MeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNReal
If `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive real factor by which `φ` scales Haar measures on `A`.
Now φ_* μ is a translation-invariant and regular measure, and hence also a
Haar measure on A. It must thus differ from μ by a positive scalar factor,
which we call d_A(φ).
There is a choice of normalization here between d_A(\phi) and
d_A(\phi)^{-1}, so let us be more precise.
To give an example, if φ is multiplication by 2 on the real numbers, if
X = [0,1], and if μ is Lebesgue measure on the Borel subsets of \R, we
have that φ_* μ(X) = μ(φ^{-1}(X)) = μ([0,1/2]) = 1/2, so
1 = d_A(\phi)/2, meaning that d_A(\phi) = 2. Similarly if φ is
multiplication by -2 and X = [0,1] then φ^{-1}(X) = [-1/2,0], which
again has measure 1/2, so d_A(\phi) is 2 again.
Strictly speaking our definition of d_A(φ) depends on the choice of regular
Haar measure \mu. Note that mathlib offers a fixed Borel regular Haar
measure MeasureTheory.Measure.haar on any locally compact topological group,
and the actual definition of d_A in the code uses this definition. Note also
that the code defines everything for multiplicative groups and uses
@[to_additive] to deduce the corresponding results for additive groups.
- Definition 10.2.1.1
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.addEquivAddHaarChar_eq[complete]
d_A(\phi) is independent of choice of regular Haar measure.
Lean code for Lemma10.2.1.2●1 theorem
Associated Lean declarations
-
MeasureTheory.addEquivAddHaarChar_eq[complete]
-
MeasureTheory.addEquivAddHaarChar_eq[complete]
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_eq.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ = μ.addHaarScalarFactor (MeasureTheory.Measure.map (⇑φ) μ)
theorem MeasureTheory.addEquivAddHaarChar_eq.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ = μ.addHaarScalarFactor (MeasureTheory.Measure.map (⇑φ) μ)
If μ' is a second choice then μ' = λ μ for some positive real λ, and the
λs on each side of μ'(X) = d_A(\phi)(\phi_* μ')(X) cancel.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If μ is any regular Haar measure on A then
d_A(\phi)(\phi_*\mu) = \mu.
Lean code for Lemma10.2.1.3●1 theorem
Associated Lean declarations
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_smul_map.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ • MeasureTheory.Measure.map (⇑φ) μ = μ
theorem MeasureTheory.addEquivAddHaarChar_smul_map.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ • MeasureTheory.Measure.map (⇑φ) μ = μ
This is a restatement of the previous result.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If μ is any regular Haar measure on A then
d_A(φ)μ = \phi^*μ.
Lean code for Corollary10.2.1.4●1 theorem
Associated Lean declarations
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_smul_eq_comap.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ • μ = MeasureTheory.Measure.comap (⇑φ) μ
theorem MeasureTheory.addEquivAddHaarChar_smul_eq_comap.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ • μ = MeasureTheory.Measure.comap (⇑φ) μ
This follows from the pushforward formula Lemma 10.2.1.3
applied to the regular Haar measure
\phi^* \mu and the fact that \phi_*\phi^*\mu = \mu.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.addEquivAddHaarChar_refl[complete]
d_A(id)=1.
Lean code for Lemma10.2.1.5●1 theorem
Associated Lean declarations
-
MeasureTheory.addEquivAddHaarChar_refl[complete]
-
MeasureTheory.addEquivAddHaarChar_refl[complete]
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_refl.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.refl G) = 1
theorem MeasureTheory.addEquivAddHaarChar_refl.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.refl G) = 1
Clear.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If X is a Borel set, then μ(X) = d_A(φ) μ(φ⁻¹(X)).
Lean code for Lemma10.2.1.6●1 theorem
Associated Lean declarations
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_smul_preimage.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {X : Set G} (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ • μ (⇑φ ⁻¹' X) = μ X
theorem MeasureTheory.addEquivAddHaarChar_smul_preimage.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {X : Set G} (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ • μ (⇑φ ⁻¹' X) = μ X
This follows immediately from lemma MeasureTheory.addEquivAddHaarChar_smul_map
and the definition of the pushforward of a measure.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If f : A → ℝ is a Borel measurable function then
d_A(φ) ∫ f(x) d(φ_* μ)(x) = ∫ f(x) dμ(x).
Lean code for Lemma10.2.1.7●1 theorem
Associated Lean declarations
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_smul_integral_map.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ • ∫ (a : G), f a ∂MeasureTheory.Measure.map (⇑φ) μ = ∫ (a : G), f a ∂μ
theorem MeasureTheory.addEquivAddHaarChar_smul_integral_map.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ+ G) : MeasureTheory.addEquivAddHaarChar φ • ∫ (a : G), f a ∂MeasureTheory.Measure.map (⇑φ) μ = ∫ (a : G), f a ∂μ
This also follows immediately from lemma.
We also have the following variant:
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If f : A → ℝ is a Borel measurable function then
d_A(φ) ∫ f(x) dμ(x) = ∫ f(x) d(φ^*μ)(x).
Lean code for Lemma10.2.1.8●1 theorem
Associated Lean declarations
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ+ G) : ∫ (a : G), f a ∂MeasureTheory.Measure.comap (⇑φ) μ = MeasureTheory.addEquivAddHaarChar φ • ∫ (a : G), f a ∂μ
theorem MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ+ G) : ∫ (a : G), f a ∂MeasureTheory.Measure.comap (⇑φ) μ = MeasureTheory.addEquivAddHaarChar φ • ∫ (a : G), f a ∂μ
This is immediate from corollary Corollary 10.2.1.4.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.addEquivAddHaarChar_trans[complete]
d_A(\phi\circ\psi)=d_A(\phi)d_A(\psi).
Lean code for Lemma10.2.1.9●1 theorem
Associated Lean declarations
-
MeasureTheory.addEquivAddHaarChar_trans[complete]
-
MeasureTheory.addEquivAddHaarChar_trans[complete]
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_trans.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] {φ ψ : G ≃ₜ+ G} : MeasureTheory.addEquivAddHaarChar (ψ.trans φ) = MeasureTheory.addEquivAddHaarChar ψ * MeasureTheory.addEquivAddHaarChar φ
theorem MeasureTheory.addEquivAddHaarChar_trans.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] {φ ψ : G ≃ₜ+ G} : MeasureTheory.addEquivAddHaarChar (ψ.trans φ) = MeasureTheory.addEquivAddHaarChar ψ * MeasureTheory.addEquivAddHaarChar φ
Here's one way: it suffices to prove that
d_A(\phi\circ\psi)(\phi\circ\psi)_*\mu = d_A(\phi)d_A(\psi)(\phi\circ\psi)_*\mu
(because there exists a compact set with positive finite measure), and using
lemma Lemma 10.2.1.3 and the fact that
(\phi\circ\psi)_*\mu = \phi_*(\psi_*\mu), one can simplify both sides to μ.
10.3. Examples
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar_real[complete]
If R=\R then \delta_R(u)=|u|.
Lean code for Lemma10.3.1●1 theorem
Associated Lean declarations
-
MeasureTheory.ringHaarChar_real[complete]
-
MeasureTheory.ringHaarChar_real[complete]
-
theoremdefined in FLT/HaarMeasure/HaarChar/RealComplex.leancomplete
theorem MeasureTheory.ringHaarChar_real (x : ℝˣ) : MeasureTheory.ringHaarChar x = ‖↑x‖₊
theorem MeasureTheory.ringHaarChar_real (x : ℝˣ) : MeasureTheory.ringHaarChar x = ‖↑x‖₊
The distributive Haar character of the action of `ℝˣ` on `ℝ` is the usual norm. This means that `volume (x • s) = ‖x‖ * volume s` for all `x : ℝ` and `s : Set ℝ`. See `Real.volume_real_smul`.
Take \mu to be Lebesgue measure and X = [0,1]. We have
δ(u) = \mu(uX). If u > 0 then u[0,1] = [0,u], which has measure
u = |u|, and if u < 0 then u[0,1] = [u,0], which has measure -u = |u|.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar_complex[complete]
If R=\bbC then \delta_R(u)=|u|^2.
Lean code for Lemma10.3.2●1 theorem
Associated Lean declarations
-
MeasureTheory.ringHaarChar_complex[complete]
-
MeasureTheory.ringHaarChar_complex[complete]
-
theoremdefined in FLT/HaarMeasure/HaarChar/RealComplex.leancomplete
theorem MeasureTheory.ringHaarChar_complex (z : ℂˣ) : MeasureTheory.ringHaarChar z = ‖↑z‖₊ ^ 2
theorem MeasureTheory.ringHaarChar_complex (z : ℂˣ) : MeasureTheory.ringHaarChar z = ‖↑z‖₊ ^ 2
The distributive Haar character of the action of `ℂˣ` on `ℂ` is the usual norm squared. This means that `volume (z • s) = ‖z‖ ^ 2 * volume s` for all `z : ℂ` and `s : Set ℂ`. See `Complex.volume_complex_smul`.
Multiplication by a positive real r sends a unit square to a square of area
r^2 = |r|^2. Multiplication by e^{i\theta} is a rotation and thus does not
change area. The general case follows.
10.3.1. Scaling Haar Measure On A Ring
Now let R be a locally compact topological ring. The Haar character of
R, or more precisely the left Haar character of R, is a group homomorphism
R^\times \to \R^\times defined in the following way. If u ∈ R^\times then
left multiplication by u, namely the map \ell_u : (R,+) → (R,+) defined by
\ell_u(r) = ur, is a homeomorphism and an additive automorphism of (R,+),
so the preceding theory applies to \ell_u.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar[complete]
We define δ_R(u), or just δ(u) when the ring R is clear, to be
d_R(ℓ_u).
Lean code for Definition10.3.1.1●1 definition
Associated Lean declarations
-
MeasureTheory.ringHaarChar[complete]
-
MeasureTheory.ringHaarChar[complete]
-
defdefined in FLT/HaarMeasure/HaarChar/Ring.leancomplete
def MeasureTheory.ringHaarChar.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Rˣ →ₜ* NNReal
def MeasureTheory.ringHaarChar.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Rˣ →ₜ* NNReal
`ringHaarChar : Rˣ →ₜ* ℝ≥0` is the function sending a unit of a locally compact topological ring `R` to the positive real factor which left multiplication by the unit scales additive Haar measure by.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar_mul_integral[complete]
If f:R\to\R is a Borel measurable function and u\in R^\times then
\delta_R(u)\int f(ux)d\mu(x)=\int f(x)d\mu(x).
Lean code for Lemma10.3.1.2●1 theorem
Associated Lean declarations
-
MeasureTheory.ringHaarChar_mul_integral[complete]
-
MeasureTheory.ringHaarChar_mul_integral[complete]
-
theoremdefined in FLT/HaarMeasure/HaarChar/Ring.leancomplete
theorem MeasureTheory.ringHaarChar_mul_integral.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (μ : MeasureTheory.Measure R) [μ.IsAddHaarMeasure] [μ.Regular] {f : R → ℝ} (hf : Measurable f) (u : Rˣ) : ↑(MeasureTheory.ringHaarChar u) * ∫ (r : R), f (↑u * r) ∂μ = ∫ (a : R), f a ∂μ
theorem MeasureTheory.ringHaarChar_mul_integral.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (μ : MeasureTheory.Measure R) [μ.IsAddHaarMeasure] [μ.Regular] {f : R → ℝ} (hf : Measurable f) (u : Rˣ) : ↑(MeasureTheory.ringHaarChar u) * ∫ (r : R), f (↑u * r) ∂μ = ∫ (a : R), f a ∂μ
A short calculation using lemma.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar_mul_volume[complete]
If X is a Borel subset of R and r ∈ R^\times, then
μ(rX) = δ_R(r) μ(X).
Lean code for Lemma10.3.1.3●1 theorem
Associated Lean declarations
-
MeasureTheory.ringHaarChar_mul_volume[complete]
-
MeasureTheory.ringHaarChar_mul_volume[complete]
-
theoremdefined in FLT/HaarMeasure/HaarChar/Ring.leancomplete
theorem MeasureTheory.ringHaarChar_mul_volume.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (μ : MeasureTheory.Measure R) [μ.IsAddHaarMeasure] [μ.Regular] {X : Set R} (u : Rˣ) : μ (u • X) = ↑(MeasureTheory.ringHaarChar u) * μ X
theorem MeasureTheory.ringHaarChar_mul_volume.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] (μ : MeasureTheory.Measure R) [μ.IsAddHaarMeasure] [μ.Regular] {X : Set R} (u : Rˣ) : μ (u • X) = ↑(MeasureTheory.ringHaarChar u) * μ X
Immediate from lemma.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar_continuous[complete]
The function δ_R : R^\times → ℝ_{>0} is continuous.
Lean code for Corollary10.3.1.4●1 theorem
Associated Lean declarations
-
MeasureTheory.ringHaarChar_continuous[complete]
-
MeasureTheory.ringHaarChar_continuous[complete]
-
theoremdefined in FLT/HaarMeasure/HaarChar/Ring.leancomplete
theorem MeasureTheory.ringHaarChar_continuous.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Continuous fun u ↦ MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u)
theorem MeasureTheory.ringHaarChar_continuous.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Continuous fun u ↦ MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u)
Fix a Haar measure \mu on R and a continuous real-valued function f on
R with compact support and such that \int f(x) d\mu(x)\not=0. Then
r \mapsto \int f(rx) d\mu(x) is a continuous function from R\to\R,
because a continuous function with compact support is uniformly continuous, and
thus gives a continuous function R^\times\to\R. Thus the function
u\mapsto(\int f(ux)d\mu(x))/(\int f(x)d\mu(x)) is a continuous function from
R^\times to \R taking values in \R_{>0}. Hence \delta_R^{-1} is
continuous from lemma, and thus \delta_R is too.
If R=\Q_p then \delta_R(u)=|u|_p, the usual p-adic norm.
Normalize Haar measure so that μ(\Z_p)=1. If u is a p-adic unit then
u\Z_p=\Z_p so multiplication by u does not change Haar measure. If however
u = p then u\Z_p has index p in \Z_p, and because
μ(i+p\Z_p)=μ(p\Z_p) we have that μ(\Z_p)=pμ(p\Z_p) and thus
δ(p)=p^{-1}. These elements generate \Q_p^\times, and two characters
which agree on generators of a group must agree on the group.
If R is a finite extension of \Q_p then \delta_R(u)
is the norm on R normalised in the following way:
\delta_R(\varpi)=q^{-1}, where \varpi is a uniformiser
and q is the size of the (finite) residue field.
10.4. Algebras
Say F is a locally compact topological ring, for example \R, \bbC,
\Q_p, or the adeles of a number field, V is a finite free F-module, and
φ : V → V is an invertible F-linear map. Then V with its module topology
(which is the product topology if one picks a basis) is a locally compact
topological abelian group, and φ is additive. One can check that linearity
implies continuity, this is IsModuleTopology.continuous_of_linearMap in
mathlib, so in fact φ is a homeomorphism and our theory applies. The
following lemma gives a formula for the scale factor d_V(φ).
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
Assume that there's an F-basis for V such that \phi is a product of
elementary and diagonal matrices, note that this is automatic if F is a field
and mathlib has this. Then d_V(\phi)=\delta_F(\det(\phi)), where
\det(\phi)\in F is the determinant of \phi as an F-linear map.
Lean code for Lemma10.4.1●2 theorems
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/FiniteDimensional.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det.{u_2, u_3} {F : Type u_2} [MeasurableSpace F] [TopologicalSpace F] [BorelSpace F] [LocallyCompactSpace F] [Field F] [IsTopologicalRing F] {V : Type u_3} [AddCommGroup V] [TopologicalSpace V] [MeasurableSpace V] [BorelSpace V] [Module F V] [FiniteDimensional F V] [IsModuleTopology F V] [IsTopologicalAddGroup V] [LocallyCompactSpace V] [SecondCountableTopology F] (ρ : V ≃L[F] V) : MeasureTheory.addEquivAddHaarChar ρ.toContinuousAddEquiv = MeasureTheory.ringHaarChar (LinearEquiv.det ↑ρ)
theorem MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det.{u_2, u_3} {F : Type u_2} [MeasurableSpace F] [TopologicalSpace F] [BorelSpace F] [LocallyCompactSpace F] [Field F] [IsTopologicalRing F] {V : Type u_3} [AddCommGroup V] [TopologicalSpace V] [MeasurableSpace V] [BorelSpace V] [Module F V] [FiniteDimensional F V] [IsModuleTopology F V] [IsTopologicalAddGroup V] [LocallyCompactSpace V] [SecondCountableTopology F] (ρ : V ≃L[F] V) : MeasureTheory.addEquivAddHaarChar ρ.toContinuousAddEquiv = MeasureTheory.ringHaarChar (LinearEquiv.det ↑ρ)
Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming `[SecondCountableTopology F]`.
-
theoremdefined in FLT/HaarMeasure/HaarChar/FiniteDimensional.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc.{u_2, u_3} {F : Type u_2} [MeasurableSpace F] [TopologicalSpace F] [BorelSpace F] [LocallyCompactSpace F] [CommRing F] [IsTopologicalRing F] {V : Type u_3} [AddCommGroup V] [TopologicalSpace V] [MeasurableSpace V] [BorelSpace V] [Module F V] [IsModuleTopology F V] [IsTopologicalAddGroup V] [LocallyCompactSpace V] [SecondCountableTopology F] (ρ : V ≃L[F] V) (n : ℕ) (b : Module.Basis (Fin n) F V) (hρ : Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec ((LinearMap.toMatrix b b) ↑↑ρ)) : MeasureTheory.addEquivAddHaarChar ρ.toContinuousAddEquiv = MeasureTheory.ringHaarChar (LinearEquiv.det ↑ρ)
theorem MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc.{u_2, u_3} {F : Type u_2} [MeasurableSpace F] [TopologicalSpace F] [BorelSpace F] [LocallyCompactSpace F] [CommRing F] [IsTopologicalRing F] {V : Type u_3} [AddCommGroup V] [TopologicalSpace V] [MeasurableSpace V] [BorelSpace V] [Module F V] [IsModuleTopology F V] [IsTopologicalAddGroup V] [LocallyCompactSpace V] [SecondCountableTopology F] (ρ : V ≃L[F] V) (n : ℕ) (b : Module.Basis (Fin n) F V) (hρ : Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec ((LinearMap.toMatrix b b) ↑↑ρ)) : MeasureTheory.addEquivAddHaarChar ρ.toContinuousAddEquiv = MeasureTheory.ringHaarChar (LinearEquiv.det ↑ρ)
Haar measure scaling for invertible linear maps on a finite-dimensional vector space over a field F assuming `[SecondCountableTopology F]`.
The proof is a generalization of
Real.map_matrix_volume_pi_eq_smul_volume_pi, which crucially uses the
induction principle
Matrix.diagonal_transvection_induction_of_det_ne_zero. One checks it
explicitly for diagonal matrices and for matrices which are the identity except
that one off-diagonal entry is non-zero.
Note: we assume that F is second countable, but it shouldn't be necessary.
Now say F is a locally compact topological field, and that R is a
possibly noncommutative F-algebra. Recall that this means that F lies in
the center of R, unless R = 0. Assume that R is finite-dimensional as an
F-vector space. Then if we give R the F-module topology, which is just
the product topology if we pick a basis, it is known that R becomes a
topological ring. Now say u ∈ R^\times, and recall that \ell_u : R → R is
left multiplication by u. Then \ell_u is easily checked to be an F-linear
homeomorphism.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If u\in R^\times then \delta_R(u)=\delta_F(\det(\ell_u)).
Lean code for Corollary10.4.2●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/FiniteDimensional.leancomplete
theorem MeasureTheory.algebra_ringHaarChar_eq_ringHaarChar_det.{u_1, u_2} (F : Type u_1) [Field F] [MeasurableSpace F] [TopologicalSpace F] [BorelSpace F] [IsTopologicalRing F] [LocallyCompactSpace F] {A : Type u_2} [Ring A] [TopologicalSpace A] [Algebra F A] [FiniteDimensional F A] [IsModuleTopology F A] [IsTopologicalRing A] [LocallyCompactSpace A] [MeasurableSpace A] [BorelSpace A] [SecondCountableTopology F] (u : Aˣ) : MeasureTheory.ringHaarChar u = MeasureTheory.ringHaarChar (LinearEquiv.det (LinearEquiv.mulLeft F u))
theorem MeasureTheory.algebra_ringHaarChar_eq_ringHaarChar_det.{u_1, u_2} (F : Type u_1) [Field F] [MeasurableSpace F] [TopologicalSpace F] [BorelSpace F] [IsTopologicalRing F] [LocallyCompactSpace F] {A : Type u_2} [Ring A] [TopologicalSpace A] [Algebra F A] [FiniteDimensional F A] [IsModuleTopology F A] [IsTopologicalRing A] [LocallyCompactSpace A] [MeasurableSpace A] [BorelSpace A] [SecondCountableTopology F] (u : Aˣ) : MeasureTheory.ringHaarChar u = MeasureTheory.ringHaarChar (LinearEquiv.det (LinearEquiv.mulLeft F u))
Follows immediately from the preceding lemma.
10.5. Left and right multiplication
If R is a locally compact topological ring, and if multiplication on R is
not commutative, then left and right multiplication by an element of R can
scale Haar measure in different ways. For example if R is the upper-triangular
2 \times 2 matrices with real entries, then left multiplication by
\begin{pmatrix}a&0\\0&1\end{pmatrix} sends
\begin{pmatrix}x&y\\0&z\end{pmatrix} to
\begin{pmatrix}ax&ay\\0&z\end{pmatrix} and thus scales R's additive Haar
measure by |a|^2, but right multiplication by
\begin{pmatrix}a&0\\0&1\end{pmatrix} sends
\begin{pmatrix}x&y\\0&z\end{pmatrix} to
\begin{pmatrix}ax&y\\0&z\end{pmatrix} and thus scales R's additive Haar
measure by a factor of |a|.
What's going on here is that if we regard left and right multiplication as
\R-linear maps from R to R, then their associated matrices with respect
to the obvious basis are diag(a,a,1) and diag(a,1,1), which have different
determinants.
However, if k is now any field and if B is a finite-dimensional central
simple algebra over k, for example a quaternion algebra, the case we'll care
about later, and if u\in B^\times then x\mapsto ux and x\mapsto xu
are both k-linear endomorphisms of B, and I claim that they have the same
determinant.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
IsSimpleRing.mulLeft_det_eq_mulRight_det[complete]
Say B is a finite-dimensional central simple algebra over a field k, and
u ∈ B^\times. Let \ell_u : B → B be the k-linear map sending x to
ux, and let r_u : B → B be the k-linear map sending x to xu. Then
det(\ell_u)=det(r_u).
Lean code for Lemma10.5.1●1 theorem
Associated Lean declarations
-
IsSimpleRing.mulLeft_det_eq_mulRight_det[complete]
-
IsSimpleRing.mulLeft_det_eq_mulRight_det[complete]
-
theoremdefined in FLT/Mathlib/LinearAlgebra/Determinant.leancomplete
theorem IsSimpleRing.mulLeft_det_eq_mulRight_det.{u_1, u_2} (k : Type u_1) [Field k] {D : Type u_2} [Ring D] [Algebra k D] [Algebra.IsCentral k D] [IsSimpleRing D] [FiniteDimensional k D] (d : D) : LinearMap.det (LinearMap.mulLeft k d) = LinearMap.det (LinearMap.mulRight k d)
theorem IsSimpleRing.mulLeft_det_eq_mulRight_det.{u_1, u_2} (k : Type u_1) [Field k] {D : Type u_2} [Ring D] [Algebra k D] [Algebra.IsCentral k D] [IsSimpleRing D] [FiniteDimensional k D] (d : D) : LinearMap.det (LinearMap.mulLeft k d) = LinearMap.det (LinearMap.mulRight k d)
Determinants are unchanged by base extension, so without loss of generality k
is algebraically closed. Then B is a matrix algebra, say M_n(k). Now u
can be thought of as a matrix with intrinsic determinant d, and B as a
left B-module becomes a direct sum of n copies of the standard
n-dimensional representation V of B. Thus det(\ell_u)=d^n. Similarly
det(r_u)=d^n, so they are equal.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If B is a central simple algebra over a locally compact field F, and if
u\in B^\times, then d_B(r_u)=\delta_B(u), recalling that the latter is
defined to mean d_B(\ell_u).
Lean code for Corollary10.5.2●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/FiniteDimensional.leancomplete
theorem IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRight.{u_1, u_2} {F : Type u_1} [Field F] [MeasurableSpace F] [TopologicalSpace F] [BorelSpace F] [IsTopologicalRing F] [LocallyCompactSpace F] {D : Type u_2} [Ring D] [TopologicalSpace D] [Algebra F D] [FiniteDimensional F D] [IsSimpleRing D] [IsModuleTopology F D] [Algebra.IsCentral F D] [IsTopologicalRing D] [LocallyCompactSpace D] [MeasurableSpace D] [BorelSpace D] [SecondCountableTopology F] (u : Dˣ) : MeasureTheory.ringHaarChar u = MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulRight u)
theorem IsSimpleRing.ringHaarChar_eq_addEquivAddHaarChar_mulRight.{u_1, u_2} {F : Type u_1} [Field F] [MeasurableSpace F] [TopologicalSpace F] [BorelSpace F] [IsTopologicalRing F] [LocallyCompactSpace F] {D : Type u_2} [Ring D] [TopologicalSpace D] [Algebra F D] [FiniteDimensional F D] [IsSimpleRing D] [IsModuleTopology F D] [Algebra.IsCentral F D] [IsTopologicalRing D] [LocallyCompactSpace D] [MeasurableSpace D] [BorelSpace D] [SecondCountableTopology F] (u : Dˣ) : MeasureTheory.ringHaarChar u = MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulRight u)
If \ell_u and r_u denote left and right multiplication by u on B, then
we have seen in lemma MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det
that d_B(r_u)=\delta_F(\det(r_u)). Lemma
IsSimpleRing.mulLeft_det_eq_mulRight_det tells us that this is
\delta_F(\det(\ell_u)), and this is \delta_B(u) again by corollary
MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det.
10.6. Finite products
Here are two facts which we will need about products.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If (A,+) and (B,+) are locally compact topological abelian groups, and if
\phi:A\to A and \psi:B\to B are additive homeomorphisms, then
\phi\times\psi:A\times B\to A\times B is an additive homeomorphism, this is
obvious, and d_{A\times B}(\phi\times\psi)=d_A(\phi)d_B(\psi).
Lean code for Lemma10.6.1●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/AddEquiv.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_prodCongr.{u_1, u_2} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] [LocallyCompactSpace H] [MeasurableSpace G] [BorelSpace G] [MeasurableSpace H] [BorelSpace H] [SecondCountableTopologyEither G H] (φ : G ≃ₜ+ G) (ψ : H ≃ₜ+ H) : MeasureTheory.addEquivAddHaarChar (φ.sumCongr ψ) = MeasureTheory.addEquivAddHaarChar φ * MeasureTheory.addEquivAddHaarChar ψ
theorem MeasureTheory.addEquivAddHaarChar_prodCongr.{u_1, u_2} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] [LocallyCompactSpace H] [MeasurableSpace G] [BorelSpace G] [MeasurableSpace H] [BorelSpace H] [SecondCountableTopologyEither G H] (φ : G ≃ₜ+ G) (ψ : H ≃ₜ+ H) : MeasureTheory.addEquivAddHaarChar (φ.sumCongr ψ) = MeasureTheory.addEquivAddHaarChar φ * MeasureTheory.addEquivAddHaarChar ψ
We only need this result in the case where both A and B are
second-countable, in which case Prod.borelSpace can be used to show that
Haar measure on A × B is the product of Haar measures on A and B, and
in this case the result follows easily. Without this assumption, the product of
these measures may not even be a Borel measure and one has to be more careful.
The proof in this case is explained by Gou"ezel.
Here is the idea. Let \rho be a Haar measure on A\times B. Fix sets
X\subseteq A and Y\subseteq B which are compact with nonempty
interior. We can now pull back \rho to a measure \nu on the Borel
sigma-algebra of A defined as \nu(s)=\rho(s\times Y), and this is
easily checked to be a Haar measure on A. Then
\delta_{A\times B}(a,0)\nu(X)=
\delta_{A\times B}(a,0)\rho(X\times Y)=\rho((a,0)(X\times Y))=
\rho(aX\times Y)=\nu(aX)=\delta_A(a)\nu(X).
So \delta_{A\times B}(a,0)=\delta_A(a). Similarly
\delta_{A\times B}(0,b)=\delta_B(b), and because \delta_{A\times B} is
a group homomorphism we're home.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If A_i are a finite collection of locally compact topological abelian groups,
with \phi_i : A_i → A_i additive homeomorphisms, then
d_{\prod_i A_i}(\prod_i\phi_i)=\prod_i d_{A_i}(\phi_i).
Lean code for Lemma10.6.2●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/AddEquiv.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_piCongrRight.{u_1, u_2} {ι : Type u_1} {H : ι → Type u_2} [(i : ι) → AddGroup (H i)] [(i : ι) → TopologicalSpace (H i)] [∀ (i : ι), IsTopologicalAddGroup (H i)] [∀ (i : ι), LocallyCompactSpace (H i)] [(i : ι) → MeasurableSpace (H i)] [∀ (i : ι), BorelSpace (H i)] [∀ (i : ι), SecondCountableTopology (H i)] [Fintype ι] (ψ : (i : ι) → H i ≃ₜ+ H i) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.piCongrRight ψ) = ∏ i, MeasureTheory.addEquivAddHaarChar (ψ i)
theorem MeasureTheory.addEquivAddHaarChar_piCongrRight.{u_1, u_2} {ι : Type u_1} {H : ι → Type u_2} [(i : ι) → AddGroup (H i)] [(i : ι) → TopologicalSpace (H i)] [∀ (i : ι), IsTopologicalAddGroup (H i)] [∀ (i : ι), LocallyCompactSpace (H i)] [(i : ι) → MeasurableSpace (H i)] [∀ (i : ι), BorelSpace (H i)] [∀ (i : ι), SecondCountableTopology (H i)] [Fintype ι] (ψ : (i : ι) → H i ≃ₜ+ H i) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.piCongrRight ψ) = ∏ i, MeasureTheory.addEquivAddHaarChar (ψ i)
Induction on the size of the finite set, using the previous lemma.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar_prod[complete]
If R and S are locally compact topological rings, then
\delta_{R\times S}(r,s)=\delta_R(r)\times\delta_S(s).
Lean code for Lemma10.6.3●1 theorem
Associated Lean declarations
-
MeasureTheory.ringHaarChar_prod[complete]
-
MeasureTheory.ringHaarChar_prod[complete]
-
theoremdefined in FLT/HaarMeasure/HaarChar/Ring.leancomplete
theorem MeasureTheory.ringHaarChar_prod.{u_1, u_2} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] {S : Type u_2} [Ring S] [TopologicalSpace S] [IsTopologicalRing S] [LocallyCompactSpace S] [MeasurableSpace S] [BorelSpace S] (u : Rˣ) (v : Sˣ) [SecondCountableTopologyEither R S] : MeasureTheory.ringHaarChar (MulEquiv.prodUnits.symm (u, v)) = MeasureTheory.ringHaarChar u * MeasureTheory.ringHaarChar v
theorem MeasureTheory.ringHaarChar_prod.{u_1, u_2} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] {S : Type u_2} [Ring S] [TopologicalSpace S] [IsTopologicalRing S] [LocallyCompactSpace S] [MeasurableSpace S] [BorelSpace S] (u : Rˣ) (v : Sˣ) [SecondCountableTopologyEither R S] : MeasureTheory.ringHaarChar (MulEquiv.prodUnits.symm (u, v)) = MeasureTheory.ringHaarChar u * MeasureTheory.ringHaarChar v
Follows immediately from lemma Lemma 10.6.1.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar_pi[complete]
If R_i are a finite collection of locally compact topological rings, and
u_i\in R_i^\times, then
\delta_{\prod_i R_i}((u_i)_i)=\prod_i\delta_{R_i}(u_i).
Lean code for Lemma10.6.4●1 theorem
Associated Lean declarations
-
MeasureTheory.ringHaarChar_pi[complete]
-
MeasureTheory.ringHaarChar_pi[complete]
-
theoremdefined in FLT/HaarMeasure/HaarChar/Ring.leancomplete
theorem MeasureTheory.ringHaarChar_pi.{u_2, u_3} {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Ring (A i)] [(i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsTopologicalRing (A i)] [∀ (i : ι), LocallyCompactSpace (A i)] [(i : ι) → MeasurableSpace (A i)] [∀ (i : ι), BorelSpace (A i)] [Fintype ι] [∀ (i : ι), SecondCountableTopology (A i)] (u : (i : ι) → (A i)ˣ) : MeasureTheory.ringHaarChar (MulEquiv.piUnits.symm u) = ∏ i, MeasureTheory.ringHaarChar (u i)
theorem MeasureTheory.ringHaarChar_pi.{u_2, u_3} {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Ring (A i)] [(i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsTopologicalRing (A i)] [∀ (i : ι), LocallyCompactSpace (A i)] [(i : ι) → MeasurableSpace (A i)] [∀ (i : ι), BorelSpace (A i)] [Fintype ι] [∀ (i : ι), SecondCountableTopology (A i)] (u : (i : ι) → (A i)ˣ) : MeasureTheory.ringHaarChar (MulEquiv.piUnits.symm u) = ∏ i, MeasureTheory.ringHaarChar (u i)
Follows immediately from lemma Lemma 10.6.2.
10.7. Some measure-theoretic preliminaries
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
Let A and B be locally compact topological groups, and let f : A → B be
both a group homomorphism and an open embedding. The pullback along f of a
Haar measure on B is a Haar measure on A.
Lean code for Lemma10.7.1●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/Mathlib/MeasureTheory/Group/Measure.leancomplete
theorem Topology.IsOpenEmbedding.isHaarMeasure_comap.{u_1, u_2} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [MeasurableSpace G] [MeasurableMul G] [BorelSpace G] [Group H] [TopologicalSpace H] [MeasurableSpace H] [MeasurableMul H] [BorelSpace H] {φ : G →* H} (hφ : Topology.IsOpenEmbedding ⇑φ) (μ : MeasureTheory.Measure H) [μ.IsHaarMeasure] : (MeasureTheory.Measure.comap (⇑φ) μ).IsHaarMeasure
theorem Topology.IsOpenEmbedding.isHaarMeasure_comap.{u_1, u_2} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [MeasurableSpace G] [MeasurableMul G] [BorelSpace G] [Group H] [TopologicalSpace H] [MeasurableSpace H] [MeasurableMul H] [BorelSpace H] {φ : G →* H} (hφ : Topology.IsOpenEmbedding ⇑φ) (μ : MeasureTheory.Measure H) [μ.IsHaarMeasure] : (MeasureTheory.Measure.comap (⇑φ) μ).IsHaarMeasure
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.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
Topology.IsOpenEmbedding.regular_comap[complete]
The pullback of a regular Borel measure along an open embedding is a regular Borel measure.
Lean code for Lemma10.7.2●1 theorem
Associated Lean declarations
-
Topology.IsOpenEmbedding.regular_comap[complete]
-
Topology.IsOpenEmbedding.regular_comap[complete]
-
theoremdefined in FLT/Mathlib/MeasureTheory/Measure/Regular.leancomplete
theorem Topology.IsOpenEmbedding.regular_comap.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] (φ : X → Y) (hφ : Topology.IsOpenEmbedding φ) (μ : MeasureTheory.Measure Y) [μ.Regular] : (MeasureTheory.Measure.comap φ μ).Regular
theorem Topology.IsOpenEmbedding.regular_comap.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] (φ : X → Y) (hφ : Topology.IsOpenEmbedding φ) (μ : MeasureTheory.Measure Y) [μ.Regular] : (MeasureTheory.Measure.comap φ μ).Regular
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.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
Say A is a compact topological additive group and φ : A → A is an additive
isomorphism. Then d_A(φ)=1.
Lean code for Lemma10.7.3●1 theorem
Associated Lean declarations
-
theoremdefined in Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.leancomplete
theorem MeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [CompactSpace G] (φ : G ≃ₜ* G) : MeasureTheory.mulEquivHaarChar φ = 1
theorem MeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [CompactSpace G] (φ : G ≃ₜ* G) : MeasureTheory.mulEquivHaarChar φ = 1
We have d_A(\phi)\mu(A)=\mu(A), and \mu(A) is positive and finite because
A is open and compact, using Lemma 10.2.1.6.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If f : A → B is a group homomorphism and open embedding between locally
compact topological additive groups and if α : A → A and β : B → B are
additive homeomorphisms such that the square commutes
(i.e., f ∘ α = β ∘ f), then d_A(α) = d_B(β).
Lean code for Lemma10.7.4●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/AddEquiv.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding.{u_2, u_3} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [AddGroup X] [IsTopologicalAddGroup X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [AddGroup Y] [IsTopologicalAddGroup Y] [LocallyCompactSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X →+ Y} (hf : Topology.IsOpenEmbedding ⇑f) (α : X ≃ₜ+ X) (β : Y ≃ₜ+ Y) (hComm : ∀ (x : X), f (α x) = β (f x)) : MeasureTheory.addEquivAddHaarChar α = MeasureTheory.addEquivAddHaarChar β
theorem MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding.{u_2, u_3} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [AddGroup X] [IsTopologicalAddGroup X] [LocallyCompactSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [AddGroup Y] [IsTopologicalAddGroup Y] [LocallyCompactSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X →+ Y} (hf : Topology.IsOpenEmbedding ⇑f) (α : X ≃ₜ+ X) (β : Y ≃ₜ+ Y) (hComm : ∀ (x : X), f (α x) = β (f x)) : MeasureTheory.addEquivAddHaarChar α = MeasureTheory.addEquivAddHaarChar β
Choose a regular Haar measure μ_B on B. The pullback μ_A := f^* μ_B is
also a regular Haar measure by the first two lemmas just cited. Now fix a
continuous compactly-supported function g on A with
0<\int g(a)d\mu(a)<\infty. Then
d_A(\alpha)\int g(a)d\mu_A(a)=\int g(a)d(\alpha^*\mu_A)(a) by lemma. 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
Corollary 10.2.1.4, which is
d_B(\beta)\int g(a)d\mu_A(a) by definition, and so
d_A(\alpha)=d_B(\beta) as required.
10.8. Restricted products
Now say A = \prod'_i A_i is the restricted product of a collection of types
A_i with respect to the subsets C_i. Recall that this is the subset of
∏_i A_i consisting of those elements whose ith coordinate lies in C_i
for all but finitely many i. Say B = \prod'_i B_i is the restricted
product of types B_i over the same index set, with respect to subsets D_i.
Say φ_i : A_i → B_i are functions with the property that
φ_i(C_i) ⊆ D_i for all but finitely many i. It is easily checked that the
φ_i induce a function φ := \prod'_i φ_i : A → B. It is also easily checked
that if all the A_i and B_i are groups or rings or R-modules, the C_i
and D_i are subgroups or subrings or submodules, and the φ_i are group or
ring or module homomorphisms, then φ is a group or ring or module
homomorphism. However topological facts lie a little deeper.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
Continuous.restrictedProduct_congrRight[complete]
If the A_i and B_i are topological spaces and the φ_i are continuous
functions, then the restricted product φ = \prod'_i φ_i is a continuous
function.
Lean code for Lemma10.8.1●1 theorem
Associated Lean declarations
-
Continuous.restrictedProduct_congrRight[complete]
-
Continuous.restrictedProduct_congrRight[complete]
-
theoremdefined in FLT/Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.leancomplete
theorem Continuous.restrictedProduct_congrRight.{u_1, u_2, u_3} {ι : Type u_1} {ℱ : Filter ι} {G : ι → Type u_2} {H : ι → Type u_3} {C : (i : ι) → Set (G i)} {D : (i : ι) → Set (H i)} [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] {φ : (i : ι) → G i → H i} (hφ : ∀ᶠ (i : ι) in ℱ, Set.MapsTo (φ i) (C i) (D i)) (hφcont : ∀ (i : ι), Continuous (φ i)) : Continuous (RestrictedProduct.map φ hφ)
theorem Continuous.restrictedProduct_congrRight.{u_1, u_2, u_3} {ι : Type u_1} {ℱ : Filter ι} {G : ι → Type u_2} {H : ι → Type u_3} {C : (i : ι) → Set (G i)} {D : (i : ι) → Set (H i)} [(i : ι) → TopologicalSpace (G i)] [(i : ι) → TopologicalSpace (H i)] {φ : (i : ι) → G i → H i} (hφ : ∀ᶠ (i : ι) in ℱ, Set.MapsTo (φ i) (C i) (D i)) (hφcont : ∀ (i : ι), Continuous (φ i)) : Continuous (RestrictedProduct.map φ hφ)
We use the universal property RestrictedProduct.continuous_dom of the
topology in mathlib to reduce to the claim that for all finite S, the induced
map A_S:=\prod_{i\in S}A_i\times\prod_{i\notin S}C_i\to B is continuous.
Because the inclusion A_S\to A_T is continuous for S\subseteq T, we are
reduced to checking this claim for S sufficiently large that it contains all
of the i for which \phi(C_i)\not=D_i. For such S, this map factors as
A_S\to B_S\to B, and B_S\to B is continuous, so it suffices to prove that
A_S\to B_S is continuous, but this is just a product of continuous maps.
We now focus on the case that B_i = A_i are locally compact groups,
D_i = C_i are compact open subgroups, and φ_i : A_i → A_i are group
isomorphisms and homeomorphisms sending C_i onto C_i for all but finitely
many i. Then the restricted product A := \prod' A_i of the A_i with
respect to the C_i is also a locally compact topological group, and the
restricted product φ = \prod' φ_i of the φ_i is a group isomorphism and
homeomorphism, so we can ask how d_A(φ) compares to the d_{A_i}(φ_i).
First note that d_{A_i}(φ_i) = 1 for all the i such that
φ_i(C_i) = C_i, as d_{A_i}(φ_i) can be computed as
μ(φ_i(C_i))/μ(C_i) and μ(C_i) is guaranteed to have positive finite
measure as it is open and compact. Hence the product \prod_i d_{A_i}(φ_i) is
a finite product, in the sense that all but finitely many terms are 1. The
following theorem shows that the value of this product is d(φ).
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
With A, A_i, C_i, \phi_i, \phi defined as above, we have
\delta_A(\phi)=\prod_i\delta_{A_i}(\phi_i).
Lean code for Theorem10.8.2●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/AddEquiv.leancomplete
theorem MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight.{u_1, u_2} {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), IsTopologicalAddGroup (G i)] {C : (i : ι) → AddSubgroup (G i)} [hCopen : Fact (∀ (i : ι), IsOpen ↑(C i))] [hCcompact : ∀ (i : ι), CompactSpace ↥(C i)] [(i : ι) → MeasurableSpace (G i)] [∀ (i : ι), BorelSpace (G i)] [∀ (i : ι), LocallyCompactSpace (G i)] [∀ (i : ι), SecondCountableTopology (G i)] [∀ (i : ι), WeaklyLocallyCompactSpace (G i)] [Countable ι] (φ : (i : ι) → G i ≃ₜ+ G i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(C i) ↑(C i)) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.restrictedProductCongrRight φ hφ) = ∏ᶠ (i : ι), MeasureTheory.addEquivAddHaarChar (φ i)
theorem MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight.{u_1, u_2} {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → AddGroup (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), IsTopologicalAddGroup (G i)] {C : (i : ι) → AddSubgroup (G i)} [hCopen : Fact (∀ (i : ι), IsOpen ↑(C i))] [hCcompact : ∀ (i : ι), CompactSpace ↥(C i)] [(i : ι) → MeasurableSpace (G i)] [∀ (i : ι), BorelSpace (G i)] [∀ (i : ι), LocallyCompactSpace (G i)] [∀ (i : ι), SecondCountableTopology (G i)] [∀ (i : ι), WeaklyLocallyCompactSpace (G i)] [Countable ι] (φ : (i : ι) → G i ≃ₜ+ G i) (hφ : ∀ᶠ (i : ι) in Filter.cofinite, Set.BijOn ⇑(φ i) ↑(C i) ↑(C i)) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.restrictedProductCongrRight φ hφ) = ∏ᶠ (i : ι), MeasureTheory.addEquivAddHaarChar (φ i)
In the Lean file we make the additional assumption that the index set over
which we're taking the product is countable, and that the A_i are second
countable. This is because in this proof we make use of an infinite product
\prod_{i\notin S} C_i of topological spaces equipped with Haar measure, so
each topological space gets equipped with the Borel sigma algebra. mathlib
then gives the product a canonical product sigma algebra which, in the case
where the index set is uncountable, may not be the Borel sigma algebra.
However we also want to use Haar measure on the product, so we need the
canonical sigma algebra on this product to be the Borel sigma algebra. Rather
than taking the trouble to locally turn off this product sigma algebra
construction in FLT, we simply restrict to a countable index set and add
second countability assumptions, because then the product is a Borel sigma
algebra and this is all we need in our applications to adeles.
Assume φ_i(C_i)=C_i for all i\not\in S, a finite set, and work in the
open subgroup U:=\prod_{i\in S}A_i\times\prod_{i\not\in S}C_i. Then φ
induces an automorphism \phi_S of this open subgroup U of A, and in
particular lemma tells us that \delta(\phi)=\delta_U(\phi_S). Next note
that \phi_S:U\to U can be written as a product of the automorphisms
\prod_{i\not\in S}\phi_i|_{C_i} of \prod_{i\not\in S}C_i and
\prod_{i\in S}\phi_i of \prod_{i\in S}A_i, so by lemma we have
\delta(\phi)=\delta(\prod_{i\not\in S}\phi_i|_{C_i})\times\delta(\prod_{i\in S}\phi_i).
Because \prod_{i\not\in S}C_i is a compact group we must have
\delta(\phi_{i\not\in S}\phi_i|_{C_i})=1 by lemma. Finally
\delta(\prod_{i\in S}\phi_i)=\prod_{i\in S}\delta(\phi_i) by lemma and we are
home.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If u=(u_i)_i\in R^\times, then
\delta_R(u)=\prod_i\delta_{R_i}(u_i).
Lean code for Corollary10.8.3●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/Ring.leancomplete
theorem MeasureTheory.ringHaarChar_restrictedProduct.{u_2, u_3} {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Ring (A i)] [(i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsTopologicalRing (A i)] [∀ (i : ι), LocallyCompactSpace (A i)] [(i : ι) → MeasurableSpace (A i)] [∀ (i : ι), BorelSpace (A i)] {C : (i : ι) → Subring (A i)} [hCopen : Fact (∀ (i : ι), IsOpen ↑(C i))] [hCcompact : ∀ (i : ι), CompactSpace ↥(C i)] [∀ (i : ι), SecondCountableTopology (A i)] [Countable ι] (u : (RestrictedProduct (fun i ↦ A i) (fun i ↦ ↑(C i)) Filter.cofinite)ˣ) : MeasureTheory.ringHaarChar u = ∏ᶠ (i : ι), MeasureTheory.ringHaarChar ((MulEquiv.restrictedProductUnits u) i)
theorem MeasureTheory.ringHaarChar_restrictedProduct.{u_2, u_3} {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Ring (A i)] [(i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsTopologicalRing (A i)] [∀ (i : ι), LocallyCompactSpace (A i)] [(i : ι) → MeasurableSpace (A i)] [∀ (i : ι), BorelSpace (A i)] {C : (i : ι) → Subring (A i)} [hCopen : Fact (∀ (i : ι), IsOpen ↑(C i))] [hCcompact : ∀ (i : ι), CompactSpace ↥(C i)] [∀ (i : ι), SecondCountableTopology (A i)] [Countable ι] (u : (RestrictedProduct (fun i ↦ A i) (fun i ↦ ↑(C i)) Filter.cofinite)ˣ) : MeasureTheory.ringHaarChar u = ∏ᶠ (i : ι), MeasureTheory.ringHaarChar ((MulEquiv.restrictedProductUnits u) i)
By definition of restricted product we have u_i\in C_i for all but finitely
many i. Note also that u has an inverse v=(v_i)_i with v_i\in C_i
for all but finitely many i. The fact that u_iv_i=v_iu_i=1 means that
u_i,v_i\in C_i^\times for all but finitely many i. Thus the previous
theorem MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight
applies.
10.9. Adeles
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If K is a number field and V is a K-module, then the natural isomorphism
V \otimes_K \A_K = V \otimes_{\Q} \A_{\Q} induced by the natural isomorphism
\A_K = K \otimes_K \A_{\Q} is a homeomorphism if the left-hand side has the
\A_K-module topology and the right-hand side has the \A_{\Q}-module
topology.
Lean code for Corollary10.9.1●1 definition
Associated Lean declarations
-
defdefined in FLT/NumberField/AdeleRing.leancomplete
def NumberField.AdeleRing.ModuleBaseChangeContinuousLinearEquiv.{u_1, u_2, u_3} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] (V : Type u_3) [AddCommGroup V] [Module L V] [Module K V] [Algebra K L] [IsScalarTower K L V] [Algebra (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)] [IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul (NumberField.RingOfIntegers K) K L (NumberField.RingOfIntegers L)] [FiniteDimensional L V] [FiniteDimensional K V] [Algebra (NumberField.InfiniteAdeleRing K) (NumberField.InfiniteAdeleRing L)] [Algebra (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)] [Pi.FiberwiseSMul (fun a ↦ a.comap (algebraMap K L)) NumberField.InfinitePlace.Completion NumberField.InfinitePlace.Completion] [Prod.IsProdSMul (NumberField.InfiniteAdeleRing K) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (NumberField.InfiniteAdeleRing L) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)] [Module (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct L V (NumberField.AdeleRing (NumberField.RingOfIntegers L) L))] [IsScalarTower (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L) (TensorProduct L V (NumberField.AdeleRing (NumberField.RingOfIntegers L) L))] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)] [Module.Finite (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)] : TensorProduct K V (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃L[L] TensorProduct L V (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)
def NumberField.AdeleRing.ModuleBaseChangeContinuousLinearEquiv.{u_1, u_2, u_3} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] (V : Type u_3) [AddCommGroup V] [Module L V] [Module K V] [Algebra K L] [IsScalarTower K L V] [Algebra (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)] [IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul (NumberField.RingOfIntegers K) K L (NumberField.RingOfIntegers L)] [FiniteDimensional L V] [FiniteDimensional K V] [Algebra (NumberField.InfiniteAdeleRing K) (NumberField.InfiniteAdeleRing L)] [Algebra (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)] [Pi.FiberwiseSMul (fun a ↦ a.comap (algebraMap K L)) NumberField.InfinitePlace.Completion NumberField.InfinitePlace.Completion] [Prod.IsProdSMul (NumberField.InfiniteAdeleRing K) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (NumberField.InfiniteAdeleRing L) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)] [Module (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct L V (NumberField.AdeleRing (NumberField.RingOfIntegers L) L))] [IsScalarTower (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L) (TensorProduct L V (NumberField.AdeleRing (NumberField.RingOfIntegers L) L))] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)] [Module.Finite (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)] : TensorProduct K V (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) ≃L[L] TensorProduct L V (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)
𝔸_K ⊗[K] V = 𝔸_L ⊗[L] V as topological additive groups for V an L-module and K ⊆ L number fields.
Lemma IsModuleTopology.continuous_bilinear_of_finite_left tells us that
V\otimes_K\A_K has the \A_{\Q}-module topology, and it is easily checked
that the isomorphism is \A_{\Q}-linear and hence automatically continuous.
Note that in Lean this is proved for a general extension L/K rather than
only for K/\Q.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
- No associated Lean code or declarations.
Let B be a finite-dimensional central simple K-algebra. Say u ∈ B_{\A}^\times,
and define \ell_u and r_u : B_{\A} → B_{\A} by \ell_u(x)=ux and
r_u(x)=xu. Then d_{B_{\A}}(\ell_u)=d_{B_{\A}}(r_u).
We think of B_{\A} as B\otimes_K\A_K. If u=(u_v) as v runs through the
places of K, then d_{B_{\A}}(\ell_u)=\prod_v d_{B_v}(\ell_{u_v}) by
MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight, and the
product is finite. By the central-simple-algebra formula established earlier this equals
\prod_v d_{B_v}(r_{u_v}), and again by
MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight this is
d_{B_{\A}}(r_u).
The previous theorem only applies to inner forms of matrix algebras, but the
below theorem, a generalization of the adelic product formula, is valid for any
finite-dimensional K-algebra. Before we state it let's remind ourselves of the
product formula for \Q, and restate it in the language of these Haar
characters.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
-
MeasureTheory.ringHaarChar_adeles_rat[complete]
If x\in\A_{\Q}^\times, then
\delta_{\A_{\Q}}(x)=\prod_v|x_v|_v.
Lean code for Lemma10.9.3●1 theorem
Associated Lean declarations
-
MeasureTheory.ringHaarChar_adeles_rat[complete]
-
MeasureTheory.ringHaarChar_adeles_rat[complete]
-
theoremdefined in FLT/HaarMeasure/HaarChar/AdeleRing.leancomplete
theorem MeasureTheory.ringHaarChar_adeles_rat (x : (NumberField.AdeleRing (NumberField.RingOfIntegers ℚ) ℚ)ˣ) : MeasureTheory.ringHaarChar x = MeasureTheory.ringHaarChar (MulEquiv.prodUnits x).1 * ∏ᶠ (p : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)), MeasureTheory.ringHaarChar ((MulEquiv.restrictedProductUnits (MulEquiv.prodUnits x).2) p)
theorem MeasureTheory.ringHaarChar_adeles_rat (x : (NumberField.AdeleRing (NumberField.RingOfIntegers ℚ) ℚ)ˣ) : MeasureTheory.ringHaarChar x = MeasureTheory.ringHaarChar (MulEquiv.prodUnits x).1 * ∏ᶠ (p : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)), MeasureTheory.ringHaarChar ((MulEquiv.restrictedProductUnits (MulEquiv.prodUnits x).2) p)
- Lemma 10.3.1
- Lemma 10.6.1
- Theorem 10.8.2
- «MeasureTheory.ringHaarChar_padic»
By theorem MeasureTheory.addEquivAddHaarChar_prodCongr we have
\delta_{\A_{\Q}}(x)=\delta_{\A_{\Q}^\infty}(x^\infty)\times\delta_{\R}(x_\infty).
By lemma MeasureTheory.ringHaarChar_real we have
\delta_{\R}(x_\infty)=|x|_\infty, and by theorem
MeasureTheory.addEquivAddHaarChar_restrictedProductCongrRight we have
\delta_{\A_{\Q}^\infty}=\prod_p\delta_{\Q_p}(x_p). By lemma
MeasureTheory.ringHaarChar_padic we have
\delta_{\Q_p}(x_p)=|x_p|_p, and putting everything together we get the
result.
Now \A_{\Q} is a nonzero \Q-algebra and hence we have an inclusion
\Q^\times\to\A_{\Q}^\times. Here is our reinterpretation of the product
formula.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Theorem 10.9.5
- Corollary 10.9.6
- Corollary 10.9.7
If x\in\Q^\times\subseteq\A_{\Q}^\times, then
\delta_{\A_{\Q}}(x)=1.
Lean code for Lemma10.9.4●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/AdeleRing.leancomplete
theorem MeasureTheory.ringHaarChar_adeles_units_rat_eq_one (x : ℚˣ) : MeasureTheory.ringHaarChar ((Units.map ↑(algebraMap ℚ (NumberField.AdeleRing (NumberField.RingOfIntegers ℚ) ℚ))) x) = 1
theorem MeasureTheory.ringHaarChar_adeles_units_rat_eq_one (x : ℚˣ) : MeasureTheory.ringHaarChar ((Units.map ↑(algebraMap ℚ (NumberField.AdeleRing (NumberField.RingOfIntegers ℚ) ℚ))) x) = 1
By lemma MeasureTheory.ringHaarChar_adeles_rat we have
\delta_{\A_{\Q}}(x)=\prod_v|x|_v. But the product formula says that this is
1. A quick proof: if x=\pm\prod_pp^{e_p}, then
\prod_p|x|_p=\prod_pp^{-e_p} and |x|_\infty=\prod_pp^{e_p}, so they
cancel.
Next we generalize this to finite-dimensional \Q-vector spaces.
So say V is an N-dimensional \Q-vector space, and define
V_{\A}:= V\otimes_{\Q}\A_{\Q} with its \A_{\Q}-module topology. If we
choose an isomorphism V\cong\Q^N, then V_{\A}\cong\A_{\Q}^N as an
additive topological abelian group. In particular, V_{\A} is locally compact.
Fix a \Q-linear automorphism \phi:V\to V. By base extension, φ induces
an \A_{\Q}-linear automorphism \phi_{\A} of V_{\A} which is also a
homeomorphism of V_{\A} if V_{\A} is given the module topology as an
\A_{\Q}-module. Our goal is
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Corollary 10.9.6
- Corollary 10.9.7
In the above situation, where V is a finite-dimensional \Q-vector space,
\phi : V \cong V is \Q-linear, and \phi_{\A} is the base extension to
V_{\A}:=V\otimes_{\Q}\A_{\Q} as a continuous linear endomorphism of V_{\A}
with the \A_{\Q}-module topology, we have d_{V_{\A}}(\phi_{\A})=1.
Lean code for Theorem10.9.5●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/AdeleRing.leancomplete
theorem MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one.{u_1, u_3} (K : Type u_1) [Field K] [NumberField K] (V : Type u_3) [AddCommGroup V] [Module K V] [FiniteDimensional K V] (φ : V ≃ₗ[K] V) [MeasurableSpace (TensorProduct K V (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] [BorelSpace (TensorProduct K V (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] : MeasureTheory.addEquivAddHaarChar (TensorProduct.RightActions.ContinuousLinearEquiv.baseChange K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) V V φ).toContinuousAddEquiv = 1
theorem MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one.{u_1, u_3} (K : Type u_1) [Field K] [NumberField K] (V : Type u_3) [AddCommGroup V] [Module K V] [FiniteDimensional K V] (φ : V ≃ₗ[K] V) [MeasurableSpace (TensorProduct K V (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] [BorelSpace (TensorProduct K V (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] : MeasureTheory.addEquivAddHaarChar (TensorProduct.RightActions.ContinuousLinearEquiv.baseChange K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) V V φ).toContinuousAddEquiv = 1
The original blueprint proof of this was that \phi_{\mathbb{A}} : V_{\mathbb{A}}\to
V_{\mathbb{A}} could be written as a restricted product of
\phi_v:V\otimes_{\Q}\Q_v \to V\otimes_{\Q}\Q_v, and hence by
Theorem 10.8.2 we
have
d_{V_{\A}}(\phi_{\A})=\prod_p d_{V_p}(\phi_p)\times d_{V_\infty}(\phi_\infty),
and then applying
Lemma 10.4.1 this is equal
to \prod_v\delta_{\Q_v}(\det(\phi_v))\prod_v\delta_{\Q_v}(\det(\phi))=1.
This turned out to be a nightmare to formalize, because commuting the tensor
product and the restricted product cannot be done naively, as the tensor
product is over \Q and the submodules in the restricted product defining
\A_{\Q} are not \Q-modules. So one has to choose a \Z-lattice
\Lambda in V and use the isomorphisms
V\otimes_{\mathbb{Q}}\mathbb{A}
=\Lambda\otimes_{\mathbb{Z}}\mathbb{A}
=\Lambda\otimes_{\mathbb{Z}}\mathbb{Q}_\infty\times\prod'_p[\Lambda\otimes_{\mathbb{Z}}\mathbb{Q}_p;\Lambda\otimes_{\mathbb{Z}}\mathbb{Z}_p]
=V\otimes_{\mathbb{Q}}\mathbb{Q}_\infty\times\prod'_p[V\otimes_{\mathbb{Q}}\mathbb{Q}_p;im(\Lambda\otimes_{\Z}\mathbb{Z}_p)]
and check that all of these canonical maps are continuous. One of these claims
boils down to yet another claim of the form "if you do something to the
factors and then take the restricted product, then this is topologically the
same as doing it to the restricted product", with the thing being
\Lambda\otimes_{\Z} in this case. The needed homeomorphism is recorded in
Corollary 10.9.1.
So here is the proof which we actually formalized. Say an automorphism of a
finite free R-module is nice if it is a product of transvections and diagonal
matrices with unit entries. Mathlib has the fact that if R is a field then
all automorphisms are nice, and the base change of a nice morphism is nice.
Hence \phi_{\mathbb{A}} is nice, and we can simply prove
Lemma 10.4.1 for nice
endomorphisms over a commutative ring, which gives the result immediately by
the product formula.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.7
If B is a finite-dimensional \Q-algebra, for example a number field, or a
quaternion algebra over a number field, if B_{\A} denotes the ring
B\otimes_{\Q}\A_{\Q}, and if b\in B^\times, then
\delta_{B_{\A}}(b)=1.
Lean code for Corollary10.9.6●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/AdeleRing.leancomplete
theorem NumberField.AdeleRing.units_mem_ringHaarCharacter_ker.{u_1, u_4} (K : Type u_1) [Field K] [NumberField K] (B : Type u_4) [Ring B] [Algebra K B] [FiniteDimensional K B] [MeasurableSpace (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] [BorelSpace (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] (b : Bˣ) : (Units.map ↑Algebra.TensorProduct.includeLeftRingHom) b ∈ MeasureTheory.ringHaarCharKer (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))
theorem NumberField.AdeleRing.units_mem_ringHaarCharacter_ker.{u_1, u_4} (K : Type u_1) [Field K] [NumberField K] (B : Type u_4) [Ring B] [Algebra K B] [FiniteDimensional K B] [MeasurableSpace (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] [BorelSpace (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] (b : Bˣ) : (Units.map ↑Algebra.TensorProduct.includeLeftRingHom) b ∈ MeasureTheory.ringHaarCharKer (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))
Left multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure. In other words, Bˣ is in the kernel of the `ringHaarChar` of `B ⊗ 𝔸_K`.
Follows immediately from the previous theorem.
- Definition 10.2.1.1
- Lemma 10.2.1.2
- Lemma 10.2.1.3
- Corollary 10.2.1.4
- Lemma 10.2.1.5
- Lemma 10.2.1.6
- Lemma 10.2.1.7
- Lemma 10.2.1.8
- Lemma 10.2.1.9
- Lemma 10.3.1
- Lemma 10.3.2
- Definition 10.3.1.1
- Lemma 10.3.1.2
- Lemma 10.3.1.3
- Corollary 10.3.1.4
- Lemma 10.4.1
- Corollary 10.4.2
- Lemma 10.5.1
- Corollary 10.5.2
- Lemma 10.6.1
- Lemma 10.6.2
- Lemma 10.6.3
- Lemma 10.6.4
- Lemma 10.7.1
- Lemma 10.7.2
- Lemma 10.7.3
- Lemma 10.7.4
- Lemma 10.8.1
- Theorem 10.8.2
- Corollary 10.8.3
- Corollary 10.9.1
- Theorem 10.9.2
- Lemma 10.9.3
- Lemma 10.9.4
- Theorem 10.9.5
- Corollary 10.9.6
If B is a finite-dimensional \Q-algebra and if b\in B^\times, then
right multiplication by b does not change Haar measure on B_{\A}.
Lean code for Corollary10.9.7●1 theorem
Associated Lean declarations
-
theoremdefined in FLT/HaarMeasure/HaarChar/AdeleRing.leancomplete
theorem NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one.{u_1, u_4} (K : Type u_1) [Field K] [NumberField K] (B : Type u_4) [Ring B] [Algebra K B] [FiniteDimensional K B] [MeasurableSpace (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] [BorelSpace (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] (b : Bˣ) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulRight ((Units.map ↑Algebra.TensorProduct.includeLeftRingHom) b)) = 1
theorem NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one.{u_1, u_4} (K : Type u_1) [Field K] [NumberField K] (B : Type u_4) [Ring B] [Algebra K B] [FiniteDimensional K B] [MeasurableSpace (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] [BorelSpace (TensorProduct K B (NumberField.AdeleRing (NumberField.RingOfIntegers K) K))] (b : Bˣ) : MeasureTheory.addEquivAddHaarChar (ContinuousAddEquiv.mulRight ((Units.map ↑Algebra.TensorProduct.includeLeftRingHom) b)) = 1
Right multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure.
Follows immediately from the previous theorem.