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 #
-
MeasureTheory.IsFundamentalDomain.smulInvariantMeasure_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 ⧸ Γ. -
MeasureTheory.IsFundamentalDomain.isMulLeftInvariant_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/Γ.
Equations
- (_ : MeasurableVAdd G (G ⧸ Γ)) = (_ : MeasurableVAdd G (G ⧸ Γ))
Measurability of the action of the topological group G on the left-coset space G/Γ.
Equations
- (_ : MeasurableSMul G (G ⧸ Γ)) = (_ : MeasurableSMul G (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 ⧸ Γ.
Equations
- (_ : motive h) = (_ : motive h)
Instances For
The essSup of a function g on the additive quotient space G ⧸ Γ with respect
to the pushforward of the restriction, μ_𝓕, of a right-invariant measure μ to a fundamental
domain 𝓕, is the same as the essSup of g's lift to the universal cover G with respect
to μ.
The essSup of a function g on the quotient space G ⧸ Γ with respect to the pushforward
of the restriction, μ_𝓕, of a right-invariant measure μ to a fundamental domain 𝓕, is the
same as the essSup of g's lift to the universal cover G with respect to μ.
Given an additive quotient space G ⧸ Γ where Γ is Countable, and the
restriction, μ_𝓕, of a right-invariant measure μ on G to a fundamental domain 𝓕, a set
in the quotient which has μ_𝓕-measure zero, also has measure zero under the
folding of μ under the quotient. Note that, if Γ is infinite, then the folded map
will take the value ∞ on any open set in the quotient!
Given a quotient space G ⧸ Γ where Γ is Countable, and the restriction,
μ_𝓕, of a right-invariant measure μ on G to a fundamental domain 𝓕, a set
in the quotient which has μ_𝓕-measure zero, also has measure zero under the
folding of μ under the quotient. Note that, if Γ is infinite, then the folded map
will take the value ∞ on any open set in the quotient!
This is a simple version of the Unfolding Trick: Given a subgroup Γ of an
additive group G, the integral of a function f on G with respect to a right-invariant
measure μ is equal to the integral over the quotient G ⧸ Γ of the automorphization of f.
This is a simple version of the Unfolding Trick: Given a subgroup Γ of a group G, the
integral of a function f on G with respect to a right-invariant measure μ is equal to the
integral over the quotient G ⧸ Γ of the automorphization of f.
This is the Unfolding Trick: Given a subgroup Γ of a group G, the integral of a
function f on G times the lift to G of a function g on the quotient G ⧸ Γ with respect
to a right-invariant measure μ on G, is equal to the integral over the quotient of the
automorphization of f times g.
This is the Unfolding Trick: Given an additive subgroup Γ' of an additive group G', the
integral of a function f on G' times the lift to G' of a function g on the quotient
G' ⧸ Γ' with respect to a right-invariant measure μ on G', is equal to the integral over
the quotient of the automorphization of f times g.