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 onG
to 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 onG
to 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 ⧸ Γ
.