Alphabeta Math
LemmaStatement: 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 Fell closure of a single representation is its weak containment closure

Statement

Assume the Axiom of Choice. Let G be a topological group and let π,ρ∈G^ be irreducible strongly continuous unitary representations, viewed as points of the unitary dual with the Fell topology (The Fell topology on the unitary dual). Then ρ belongs to the Fell closure of the singleton {π} if and only if ρ is weakly contained in π, ρ≺π (Weak containment of unitary representations).

Facts & Assumptions

Given: AC; a topological group G; irreducible strongly continuous unitary representations π and ρ; the Fell topology on the unitary dual.

[F1]

A basis of neighbourhoods of ρ in the Fell topology is formed by the sets W(ρ;ϕ1,…,ϕn,Q,ϵ) consisting of the classes σ such that each ϕi is within ϵ on the compact set Q of a finite sum of functions of positive type associated to σ, where each ϕi is itself a single diagonal matrix coefficient of ρ (The Fell topology on the unitary dual, Matrix coefficient of a unitary representation, Continuous positive-type functions and normalization).

[F2]

ρ≺π means that for every ξ in the carrier of ρ, every compact Q⊆G and every ϵ>0 there are finitely many vectors η1,…,ηm in the carrier of π with sup⁡Q∣cξ,ξ−∑jcηj,ηj∣<ϵ (Weak containment of unitary representations, Matrix coefficient of a unitary representation).

Proof

technique · direct

Given: AC, a topological group G, irreducible representations π,ρ, and the Fell basis of [F1].

1.1F1

By [F1], a basic neighbourhood of ρ is determined by finitely many functions ϕ1,…,ϕn of positive type associated to ρ, a compact Q and ϵ>0, and it consists exactly of the classes σ for which each ϕi is within ϵ on Q of a finite sum of functions of positive type associated to σ. In particular the singleton {π} meets this neighbourhood if and only if π belongs to it, that is, if and only if each ϕi admits such an approximation by coefficients of π.

1.2F2algebra

It is enough to test single diagonal coefficients. If every diagonal coefficient cξ,ξ of ρ is, for every compact Q and ϵ>0, within ϵ on Q of a finite sum of coefficients of π, then so is every finite sum ϕ=∑i=1ncξi,ξi: choose for each summand an approximating finite sum with error less than ϵ/n on Q and add these finitely many identities. Conversely, a single diagonal coefficient is itself a finite sum of this form, with n=1.

2.1F1step 1.1step 1.2

Consequently, for a basic neighbourhood of ρ as in step 1.1, {π} meets it if and only if each tested ϕi is approximated by coefficients of π; by step 1.2 and the basis property of [F1], this happens for every basic neighbourhood of ρ if and only if every diagonal coefficient of ρ is approximated, uniformly on compacta, by finite sums of coefficients of π.

3.1F1F2step 2.1∎

Since a point of a topological space lies in the closure of a set S exactly when every basic neighbourhood of the point meets S, step 2.1 with S={π} gives: ρ∈{π}‾ if and only if every diagonal coefficient of ρ is approximated on compacta by finite sums of coefficients of π, which by [F2] is exactly ρ≺π. The Axiom of Choice is inherited from the unitary dual and Fell topology suppliers of [F1]; the unwinding of the neighbourhood basis uses no choice (The Axiom of Choice).

Depends on

Used by

Dependency tree · two levels

13 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