How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The modular function is a continuous homomorphism
Statement
Assume AC. The modular function of an LCH group with fixed left Haar measure is a continuous group homomorphism; that is, for all and is continuous for the usual topology of .
Facts & Assumptions
Given: An LCH group , a left Haar measure on , the modular function of Modular function of a locally compact group, and AC.
For every the translate identity with holds for and, in the Borel-level form, for every nonnegative Borel (Right translation scales left Haar measure).
is defined by the unique positive scalar of [F1], and the definition is independent of the normalisation of (Modular function of a locally compact group).
Translation preserves compact support and, at every , the maps and are continuous in uniform norm with all supports contained in a fixed compact set on a neighbourhood of (Translations preserve compactly supported continuous functions).
A left Haar measure is nonzero, Radon, positive on nonempty open sets, and finite on compact sets; a nonzero nonnegative function has strictly positive integral (Left Haar integral and left Haar measure, Haar measure is positive on nonempty open sets and finite on compact sets).
Assuming Dependent Choice, a compact set inside an open set admits with (LCH Urysohn cutoff).
Recursion: given a set , and , there is with and (The recursion theorem).
AC is assumed in the choice-function form of the cited definition (The Axiom of Choice).
Proof
Discharge the choice hypothesis of [F5] from AC. Given a set , a point and a serial relation on (every nonempty), [A1] chooses one member of each set in the family , and composing this choice function with gives with . By [F6] the recursion , produces an infinite -chain from . So Dependent Choice is available.
Multiplicativity. Fix and a Borel set with , which exists by inner regularity and finiteness on compact sets in [F4]. Using the Borel-level identity of [F1] twice gives , while the defining property of gives ; the scalar therefore annihilates the nonzero measure , so , and replacing by their inverses and using from [F2] gives .
There is with and . Since is nonzero and outer regular on Borel sets by [F4], some open has ; inner regularity of on the open set gives a compact with . By [F5], applied under the Dependent Choice just derived, choose with ; then and .
Define for for the function of step 2.1. By [F1] applied to we have for every , and by step 2.1; hence for every , so continuity of will follow from continuity of and of inversion.
The function is continuous. Fix . By [F3] there are a neighbourhood of and a compact with for every and with as ; for the difference is supported in , whence with by [F4], so .
is continuous: by step 3.1 it is the composition of the continuous maps (inversion in a topological group), the map that is continuous by step 3.2, and division by the positive constant .
Finally , because forces by the same uniqueness of the scalar as in [F1]; and takes values in by definition. With the multiplicativity of step 1.2 this exhibits as a continuous homomorphism from to the multiplicative group . ∎
Depends on
Modular function of a locally compact group
Right translation scales left Haar measure
Translations preserve compactly supported continuous functions
Haar measure is positive on nonempty open sets and finite on compact sets
Left Haar integral and left Haar measure
LCH Urysohn cutoff
The recursion theorem
The Axiom of Choice