ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Finite transitive $G$ -sets recover the stabilizer-induction classification

Example

Assume AC. Let $G$ be a finite group with the discrete topology acting transitively on a finite set $X$ , fix $x_{0} \in X$ , put $H = {Stab}_{G} (x_{0})$ and identify $X$ with $G / H$ . Let $H = ℓ^{2} (X)$ carry the permutation representation $U$ , and let $P$ be the projection-valued measure on $X$ assigning to $E \subseteq X$ the orthogonal projection onto the coordinate subspace $ℓ^{2} (E)$ . Then $(U, P)$ is a transitive system of imprimitivity on the finite standard Borel space $X$ , and it is unitarily equivalent to the canonical system of the trivial representation $1_{H}$ of $H$ ; the induced representation ${Ind}_{H}^{G} 1_{H}$ is the permutation representation on $G / H$ , so the finite case of Mackey's theorem reduces to the classical stabilizer/induction classification. More generally a finite-dimensional unitary representation of $G$ carrying a transitive system on $X$ is induced from a unitary representation of $H$ on a fibre of dimension $\dim (H) / ∣ X ∣$ , by the general theorem.

Facts & Assumptions

Given: AC, the finite group $G$ , the transitive finite $G$ -set $X$ , the stabilizer $H$ of $x_{0}$ , and the permutation representation $U$ on $ℓ^{2} (X)$ with the coordinate projections $P$ .

[F1]

The finite set $X$ with the discrete metric is Polish (every Cauchy sequence is eventually constant, the full set is dense) and its power-set $σ$ -algebra is standard Borel; unitary representations of the discrete group $G$ are strongly continuous (Polish spaces are separable completely metrizable spaces, Standard Borel spaces, Hilbert space).

[F2]

The coordinate projections $ℓ^{2} (E)$ are orthogonal projections satisfying $P (E) P (F) = P (E \cap F)$ , $P (\emptyset) = 0$ , $P (X) = I$ and finite additivity, so $P$ is a projection-valued measure; the permutation representation is unitary with $U P (E) U^{- 1} = P (g E)$ (The orthogonal projection $P_{W} v$ is the $W$ -component in $V = W \oplus W^{⊥}$ , Hilbert projections are linear, self-adjoint and contractive, Projection valued measure, Left group actions, transitive actions, and faithful actions).

[F3]

Transitivity identifies $X$ with the left coset space $G / H$ , where $H = {Stab}_{G} (x_{0})$ , and ${Ind}_{H}^{G} 1_{H}$ is the permutation representation of $G$ on $G / H$ (Left and right cosets $g H$ and $H g$ of a subgroup, Left group actions, transitive actions, and faithful actions, Inducing the trivial representation gives the permutation representation on $G / H$ , The induced $R$ -linear $G$ -module ${Ind}_{H}^{G} W$ as $H$ -covariant functions on $G$ ).

[F4]

Mackey's imprimitivity theorem and its uniqueness clause apply to the transitive system on $G / H$ : it is unitarily equivalent to the canonical induced system of a strongly continuous unitary representation of $H$ , and the inducing representation is unique up to unitary equivalence (Mackey's imprimitivity theorem, Uniqueness in the imprimitivity theorem, Systems of imprimitivity for a Borel $G$ -space, Transitive systems of imprimitivity and their normalized measure class).

[F5]

AC is the standing hypothesis (The Axiom of Choice).

Verification

technique · direct

Given: AC, the data above.

1.1F1F2F3

$(U, P)$ is a system of imprimitivity: by [F1] $U$ is a strongly continuous unitary representation on the finite-dimensional space $ℓ^{2} (X)$ , and by [F2] $P$ is a projection-valued measure with $U P (E) U^{- 1} = P (g E)$ for all $g$ and all $E \subseteq X$ . The action is transitive, so the system is transitive on the finite homogeneous space $G / H$ by [F3], which is a standard Borel space by [F1].

2.1F2F3step 1.1construct

The equivalence preserves both parts of the system. For $v \in ℓ^{2} (X)$ set $F_{v} (g) = v (g x_{0})$ . Then $F_{v} (g h) = F_{v} (g)$ for $h \in H$ , and $\sum_{g H} ∣ F_{v} (g) ∣^{2} = \sum_{x \in X} ∣ v (x) ∣^{2}$ , so this is a unitary onto the covariant model of ${Ind}_{H}^{G} 1_{H}$ with counting quotient measure. It sends $(U_{a} v) (x) = v (a^{- 1} x)$ to $F_{v} (a^{- 1} g)$ and sends $P (E)$ to multiplication by $1_{E} (g x_{0})$ . Thus the permutation system is the canonical induced system of $1_{H}$ , not merely an equivalent group representation.

3.1F2F4step 2.1algebra

Fibre dimension: for a finite-dimensional unitary representation carrying a transitive system, the fibres $P ({x}) H$ are mutually orthogonal (the singletons are disjoint) and sum to $H$ ; transitivity of $U$ transports $P ({x})$ to $P ({g x})$ , so all fibres have the same dimension $d$ ; hence $∣ X ∣ d = \dim H$ and $d = \dim (H) / ∣ X ∣$ . The general theorem identifies the representation with the induction of a unitary representation of $H$ on one fibre, of that dimension; the induced space has the original total dimension.

4.1step 1.1step 2.1step 3.1F5∎

Steps 1.1, 2.1 and 3.1 verify the claims: the permutation system is a transitive system of imprimitivity on the finite standard Borel space, it is equivalent to the canonical system of the trivial representation of the stabilizer, the finite computation of the induction is the permutation representation, and the fibre dimension of a general finite-dimensional transitive system is $\dim (H) / ∣ X ∣$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 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

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)
I. M. Isaacs, Character Theory of Finite Groups, Chapter 5 (induced characters and permutation representations) (standard reference, not scraped)

Finite transitive GG-sets recover the stabilizer-induction classification