LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 imprimitivity reconstruction map is isometric and intertwining

Statement

Assume AC. In the normalized model of a transitive system $(U, P)$ on $G / H$ , take the Borel unitaries $B$ and the stabilizer representation $σ$ supplied by the preceding lemma. Multiplication by $B$ is unitary and $(B^{- 1} W U_{g} W^{- 1} B f) (x) = D_{g} (x)^{1 / 2} σ (s (x)^{- 1} g s (g^{- 1} x)) f (g^{- 1} x) .$ This is the canonical induced action of ${Ind}_{H}^{G} σ$ . Moreover $B^{- 1} W P (E) W^{- 1} B = M_{1_{E}}$ for all Borel $E$ . Hence $(U, P)$ is unitarily equivalent to the canonical induced system by an isometric map intertwining both $U$ and $P$ .

Facts & Assumptions

Given: AC, the normalized transitive system $(U, P)$ with multiplicity model $W$ , cocycle fields $φ_{g}$ , Borel unitaries $B$ and stabilizer representation $σ$ .

[F1]

The multiplicity-normalized model is $W : H_{0} \to L^{2} (G / H, μ; K)$ with $W P (E) W^{- 1} = M_{1_{E}}$ , and the source-variable cocycle fields satisfy $W U_{g} W^{- 1} f (x) = D_{g} (x)^{1 / 2} φ_{g} (g^{- 1} x) f (g^{- 1} x)$ , where $D_{g} (x) = d (L_{g})_{*} μ / d μ (x)$ (Spectral multiplicity model of a transitive system of imprimitivity, Measurable cocycle fields for a multiplicity-normalized system, Direct integral of a measurable Hilbert field).

[F2]

The stabilizer lemma supplies, after the strict normalization, the identity $φ_{g} (x) = B (g x) σ (h (g, x)) B (x)^{- 1}$ for every $g$ and every $x$ , with $h (g, x) = s (g x)^{- 1} g s (x)$ (The stabilizer acts unitarily on an imprimitivity fibre, Borel cross-sections for closed subgroups of second-countable locally compact Hausdorff groups).

[F3]

The canonical induced model of $σ$ on the covariant completion with rho-measure $μ_{ρ}$ has action $(Π (g) F) (x) = D_{g} (x)^{1 / 2} F (g^{- 1} x)$ on covariant $F$ and is independent of the choice of rho-function and of the equivalent measure representative in the class (An induced representation carries a canonical system of imprimitivity on $G / H$ , Continuous covariant model and measurable completion, Unitary cocycle-corrected left action, Unitary induction from a closed subgroup, Independence of rho and equivalent quotient representative).

[F4]

Multiplication by a Borel field of unitary operators is unitary on the direct integral and commutes with every $M_{f}$ ; the commutant of the multiplications consists of the decomposable operators (Decomposable operators are the commutant of diagonal multiplication, Direct integral of a measurable Hilbert field).

[F5]

AC is the standing hypothesis (The Axiom of Choice, Strongly continuous unitary representations, invariant linear subspaces and intertwiners, Transitive systems of imprimitivity and their normalized measure class, Unitary equivalence of systems of imprimitivity and of the induced representations).

Proof

technique · direct

Given: AC, the normalized model with $B, σ$ and the cocycle fields.

1.1F4

Multiplication $M_{B}$ by the Borel unitary field $x \mapsto B_{x}$ is a unitary of $L^{2} (G / H, μ; K)$ by [F4], and it commutes with every $M_{f}$ because $f (x) I_{K}$ commutes with the operator $B_{x}$ in every fibre.

2.1F1F2F3step 1.1

Action computation: for $f$ in the model, using [F1] and then the strict factorization [F2] evaluated at the source point $g^{- 1} x$ , where $h (g, g^{- 1} x) = s (x)^{- 1} g s (g^{- 1} x)$ , $(M_{B}^{- 1} W U_{g} W^{- 1} M_{B} f) (x) = B_{x}^{- 1} D_{g} (x)^{1 / 2} (B_{x} σ (h (g, g^{- 1} x)) B_{g^{- 1} x}^{- 1}) B_{g^{- 1} x} f (g^{- 1} x),$ so the $B$ -factors cancel and the result is $D_{g} (x)^{1 / 2} σ (s (x)^{- 1} g s (g^{- 1} x)) f (g^{- 1} x)$ . By [F3] this is exactly the canonical induced action of ${Ind}_{H}^{G} σ$ in section coordinates: identifying a square-integrable section $f$ with the covariant function determined by $F (s (x)) = f (x)$ and $F (x h) = σ (h)^{- 1} F (x)$ , one has $F (g^{- 1} s (x)) = σ (h (g, g^{- 1} x)) F (s (g^{- 1} x))$ because $g^{- 1} s (x) = s (g^{- 1} x) h (g^{- 1}, x)$ and $h (g^{- 1}, x) = h (g, g^{- 1} x)^{- 1}$ , so the induced formula $(Π (g) F) (x) = D_{g} (x)^{1 / 2} F (g^{- 1} x)$ becomes the displayed action; the measure $μ$ lies in the class used by the induced model by [F3].

2.2F4step 1.1

PVM transport: $M_{B}$ commutes with $M_{1_{E}}$ , so $M_{B}^{- 1} W P (E) W^{- 1} M_{B} = M_{B}^{- 1} M_{1_{E}} M_{B} = M_{1_{E}}$ for every Borel $E$ .

3.1step 2.1step 2.2

Consequently the composite $Φ : = M_{B}^{- 1} W : H_{0} \to L^{2} (G / H, μ; K)$ is a unitary (a composite of unitaries), and by [step 2.1] and [step 2.2] it intertwines $U_{g}$ with the canonical induced action and $P (E)$ with multiplication by $1_{E}$ . Being unitary, $Φ$ is isometric; the target is identified with the induced space of $σ$ by [F3].

4.1step 3.1F5∎

Thus the transitive system $(U, P)$ is unitarily equivalent to the canonical induced system of $σ$ by the isometric intertwiner $Φ$ , which is the reconstruction map of the statement.

Depends on

Used by

Mackey's imprimitivity theorem Theorem
Uniqueness in the imprimitivity theorem Theorem

Dependency tree · two levels

100 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

V. S. Sunder, Notes on the Imprimitivity Theorem (ISIBangalore/IMSc lecture notes, 22 pp.) (standard reference, not scraped)
G. Misra, E. K. Narayanan and C. Varughese, Mackey Imprimitivity and commuting tuples of homogeneous normal operators, arXiv:2402.15737 (standard reference, not scraped)
G. W. Mackey, Imprimitivity for Representations of Locally Compact Groups I, PNAS 35 (1949) 537-545 (Internet Archive capture of the PubMed Central scan) (standard reference, not scraped)