CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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 unitary dual of a compact group is Fell discrete

Statement

Assume the Axiom of Choice. Let $K$ be a compact Hausdorff group with its unitary dual $\hat{K}$ (The unitary dual of a compact group, The unitary dual of a locally compact group) and the Fell topology on the dual The Fell topology on the unitary dual. Then every point of $\hat{K}$ is isolated: the singleton ${[π]}$ is open for every $π \in \hat{K}$ . Consequently $\hat{K}$ is a discrete topological space: if a net $(π_{i})$ in $\hat{K}$ converges to $π$ in the Fell topology, then $π_{i}$ is unitarily equivalent to $π$ for all sufficiently large $i$ .

Facts & Assumptions

Given: AC; a compact Hausdorff group $K$ with normalized Haar probability $μ$ ; a class $π \in \hat{K}$ with a representative on $H_{π}$ , $d_{π} = \dim_{C} H_{π}$ , fixed orthonormal basis $e_{1}^{π}, \dots, e_{d_{π}}^{π}$ ; the Fell topology on $\hat{K}$ .

[F1]

Peter-Weyl: the normalized block $B = (u_{i j}^{π})$ , $u_{i j}^{π} (k) = \sqrt{d_{π}} ⟨ π (k) e_{i}^{π}, e_{j}^{π} ⟩$ , is an orthonormal basis of $L^{2} (K)$ ; in particular $\int_{K} u_{i j}^{π} \overline{u_{k l}^{ρ}} d μ = δ_{π ρ} δ_{i k} δ_{j l}$ , so the closed spans $M_{π}$ of the coefficient blocks of two inequivalent classes are orthogonal (The normalized matrix coefficients form an orthonormal basis of L2(K), The normalized irreducible matrix coefficient family, Matrix coefficient of a unitary representation).

[F2]

A diagonal coefficient of a representation $ρ$ at a vector $η$ is a finite linear combination of matrix coefficients $⟨ ρ (k) e_{i}, e_{j} ⟩$ , and a function of positive type associated to $ρ$ is a single diagonal coefficient; hence every such function and every finite sum of them lies in $M_{ρ}$ (Continuous positive-type functions and normalization, Matrix coefficient of a unitary representation).

[F3]

Fell basis: for $π$ and data $(ϕ, Q, ϵ)$ the set $W (π; ϕ, Q, ϵ)$ of classes whose members admit a finite sum $ψ$ of functions of positive type associated to them with $\sup_{k \in Q} ∣ ϕ (k) - ψ (k) ∣ < ϵ$ is a neighbourhood of $[π]$ (taking $ϕ$ itself as witness), and these sets generate the topology (The Fell topology on the unitary dual, The unitary dual of a compact group).

[F4]

A normalized coefficient satisfies $∣ ϕ (k) ∣ \leq 1$ for all $k$ and $∥ ϕ ∥_{1} \leq 1$ since $μ$ is a probability measure (Translation estimates for continuous positive type functions).

Proof

technique · direct

Given: AC, a compact group $K$ , a class $π \in \hat{K}$ and a normalized coefficient $ϕ (k) = ⟨ π (k) ξ, ξ ⟩$ with $∥ ξ ∥ = 1$ .

1.1F1

Write $ξ = \sum_{i} a_{i} e_{i}^{π}$ with $\sum_{i} ∣ a_{i} ∣^{2} = 1$ . Then $ϕ = (1 / \sqrt{d_{π}}) \sum_{i, j} a_{i} {\overset{ˉ}{a}}_{j} u_{i j}^{π}$ , a linear combination of the orthonormal block elements of [F1] with coefficients $a_{i} {\overset{ˉ}{a}}_{j} / \sqrt{d_{π}}$ ; Parseval in the orthonormal basis gives $c : = \int_{K} ∣ ϕ ∣^{2} d μ = (1 / d_{π}) \sum_{i, j} ∣ a_{i} ∣^{2} ∣ a_{j} ∣^{2} = 1 / d_{π} > 0$ . In particular $ϕ \in M_{π}$ and $c$ is strictly positive, while $c = 1$ holds only in the one-dimensional case.

2.1F1F2step 1.1

Orthogonality to other classes: if $ρ \in \hat{K}$ is inequivalent to $π$ and $ψ$ is a finite sum of functions of positive type associated to $ρ$ , then $\int_{K} ϕ \overset{ˉ}{ψ} d μ = 0$ . Indeed $ϕ \in M_{π}$ by step 1.1 and $ψ \in M_{ρ}$ by [F2], and $M_{π} ⊥ M_{ρ}$ since the two classes are inequivalent in the Peter-Weyl orthonormal basis.

3.1F3F4step 1.1step 2.1

The Fell neighbourhood $W (π; ϕ, K, ϵ)$ with $ϵ : = c / (1 + ∥ ϕ ∥_{1}) > 0$ meets $\hat{K}$ exactly in ${[π]}$ . It contains $[π]$ by [F3]. Conversely let $[ρ] \in W$ , so there is a finite sum $ψ$ of functions of positive type associated to $ρ$ with $\sup_{K} ∣ ϕ - ψ ∣ < ϵ$ ; then $∣ \int_{K} ϕ \overset{ˉ}{ψ} d μ - c ∣ = ∣ \int_{K} ϕ (\overset{ˉ}{ψ} - \overset{ˉ}{ϕ}) d μ ∣ \leq \sup_{K} ∣ ϕ - ψ ∣ ∥ ϕ ∥_{1} < ϵ ∥ ϕ ∥_{1} < c$ by [F4], so $\int_{K} ϕ \overset{ˉ}{ψ} d μ \neq 0$ ; step 2.1 forces $ρ$ to be unitarily equivalent to $π$ . Hence $W \cap \hat{K} = {[π]}$ .

4.1F3step 3.1

By step 3.1 the singleton ${[π]}$ is the intersection with $\hat{K}$ of an open set, hence is open in the dual; therefore it is a neighbourhood of $[π]$ , so a net in $\hat{K}$ converging to $[π]$ is eventually in ${[π]}$ , and a net with limit $[π]$ is eventually equivalent to $π$ . Since $π$ was arbitrary, every point is isolated and the dual is discrete.

5.1givenF1∎

The Axiom of Choice is inherited from the choice of representatives and orthonormal bases in the Peter-Weyl family; the orthogonality computation, the choice of $ϵ$ and the separation argument add no further choice (The Axiom of Choice).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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

Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (Cambridge University Press 2008; author-hosted complete text) (standard reference, not scraped)
Bachir Bekka and Pierre de la Harpe, Unitary Representations of Groups, Duals, and Characters (arXiv:1912.07262v1, 16 December 2019) (standard reference, not scraped)