Haar quotient measure #
In this file, we consider properties of fundamental domains and measures for the action of a
subgroup of a group G on G itself.
Main results #
-
measure_theory.is_fundamental_domain.smul_invariant_measure_map: given a subgroupΓof a topological groupG, the pushforward to the coset spaceG ⧸ Γof the restriction of a both left- and right-invariant measure onGto a fundamental domain𝓕is aG-invariant measure onG ⧸ Γ. -
measure_theory.is_fundamental_domain.is_mul_left_invariant_map: given a normal subgroupΓof a topological groupG, the pushforward to the quotient groupG ⧸ Γof the restriction of a both left- and right-invariant measure onGto a fundamental domain𝓕is a left-invariant measure onG ⧸ Γ.
Note that a group G with Haar measure that is both left and right invariant is called
unimodular.
Measurability of the action of the additive topological group G on the left-coset
space G/Γ.
Measurability of the action of the topological group G on the left-coset space G/Γ.
The pushforward to the coset space G ⧸ Γ of the restriction of a both left- and
right-invariant measure on an additive topological group G to a fundamental domain 𝓕 is a
G-invariant measure on G ⧸ Γ.
The pushforward to the coset space G ⧸ Γ of the restriction of a both left- and right-
invariant measure on G to a fundamental domain 𝓕 is a G-invariant measure on G ⧸ Γ.
Assuming Γ is a normal subgroup of an additive topological group G, the
pushforward to the quotient group G ⧸ Γ of the restriction of a both left- and right-invariant
measure on G to a fundamental domain 𝓕 is a left-invariant measure on G ⧸ Γ.
Assuming Γ is a normal subgroup of a topological group G, the pushforward to the quotient
group G ⧸ Γ of the restriction of a both left- and right-invariant measure on G to a
fundamental domain 𝓕 is a left-invariant measure on G ⧸ Γ.
Given a normal subgroup Γ of an additive topological group G with Haar measure
μ, which is also right-invariant, and a finite volume fundamental domain 𝓕, the pushforward
to the quotient group G ⧸ Γ of the restriction of μ to 𝓕 is a multiple of Haar measure on
G ⧸ Γ.
Given a normal subgroup Γ of a topological group G with Haar measure μ, which is also
right-invariant, and a finite volume fundamental domain 𝓕, the pushforward to the quotient
group G ⧸ Γ of the restriction of μ to 𝓕 is a multiple of Haar measure on G ⧸ Γ.
Given a normal subgroup Γ of an additive
topological group G with Haar measure μ, which is also right-invariant, and a finite volume
fundamental domain 𝓕, the quotient map to G ⧸ Γ is measure-preserving between appropriate
multiples of Haar measure on G and G ⧸ Γ.
Given a normal subgroup Γ of a topological group G with Haar measure μ, which is also
right-invariant, and a finite volume fundamental domain 𝓕, the quotient map to G ⧸ Γ is
measure-preserving between appropriate multiples of Haar measure on G and G ⧸ Γ.