ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge 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.

Full and reduced group C star algebras of a finite group

Example

Assume the Axiom of Choice. Let $G$ be a finite group, regarded as a compact Hausdorff group, with normalized Haar probability (The unitary dual of a compact group). Then the full and reduced group C*-algebras coincide, $C^{*} (G) = C_{r}^{*} (G) ≅ ⨁_{π \in \hat{G}} End (H_{π}) ≅ ⨁_{π \in \hat{G}} M_{d_{π}} (C), d_{π} = \dim_{C} H_{π},$ a finite-dimensional semisimple C*-algebra (The full (maximal) group C star algebra, The reduced group C star algebra, ${End}_{F} (V)$ is a ring and matrix representation is a ring isomorphism ${End}_{F} (V) ≅ M_{n} (F)$ ).

Facts & Assumptions

Given: AC; a finite group $G$ ; its unitary dual $\hat{G}$ ; the left regular representation $λ$ on $L^{2} (G)$ ; the dense embedding $L^{1} (G) \to C^{*} (G)$ .

[F1]

A finite group is compact Hausdorff, and every strongly continuous unitary representation $ρ$ of $G$ is a discrete Hilbert direct sum $ρ ≅ {⨁^{^}}_{i} σ_{i}$ of finite-dimensional irreducibles $σ_{i} \in \hat{G}$ ; the dual $\hat{G}$ is finite (Unitary representations of compact groups are discrete Hilbert sums of irreducibles, The unitary dual of a compact group).

[F2]

The normalized irreducible matrix coefficient family $B = (u_{i j}^{π})_{π \in \hat{G}, 1 \leq i, j \leq d_{π}}$ is an orthonormal basis of $L^{2} (G)$ , and the left regular representation satisfies $λ ≅ {⨁^{^}}_{π \in \hat{G}} d_{π} π$ (The normalized matrix coefficients form an orthonormal basis of L2(K), Peter-Weyl decomposition of the regular representation, The normalized irreducible matrix coefficient family, Left and right regular unitary representations of an LCH group).

[F3]

For a unitary representation $π$ the integrated form $f \mapsto π (f) = \int_{G} f (g) π (g) d g$ is a $*$ -homomorphism of $L^{1} (G)$ , and unitary representations correspond to nondegenerate star-representations through this construction (Unitary representations correspond to nondegenerate star representations of L one, Nondegenerate representations of the full group C star algebra are unitary representations).

[F4]

$C^{*} (G)$ is the completion of $L^{1} (G)$ in the norm $∥ f ∥_{C^{*}} = \sup_{ρ} ∥ ρ (f) ∥$ , and $C_{r}^{*} (G)$ is the norm closure of ${λ (f) : f \in L^{1} (G)}$ in $B (L^{2} (G))$ ; the integrated form of $λ$ extends to a surjective star-homomorphism $C^{*} (G) ↠ C_{r}^{*} (G)$ which is the identity on $L^{1} (G)$ (The full (maximal) group C star algebra, The reduced group C star algebra, The canonical map from the full to the reduced group C star algebra).

[F5]

$End (H) ≅ M_{d} (C)$ as rings after a basis is chosen ( ${End}_{F} (V)$ is a ring and matrix representation is a ring isomorphism ${End}_{F} (V) ≅ M_{n} (F)$ ). Choosing an orthonormal basis for the finite-dimensional Hilbert space makes the matrix of the Hilbert adjoint the conjugate transpose: its entries satisfy $⟨ T^{*} e_{j}, e_{i} ⟩ = \overline{⟨ T e_{i}, e_{j} ⟩}$ . Thus this identification is a $*$ -isomorphism locally, rather than an extra assertion of the ring supplier.

[F6]

A unital ring is semisimple when its left regular module is a direct sum of simple submodules (A semisimple ring as a ring whose left regular module is semisimple, Semisimple modules as direct sums of simple modules).

Verification

technique · direct

Given: AC, a finite group $G$ , its unitary dual $\hat{G}$ , the regular representation $λ$ and $L^{1} (G) \subseteq C^{*} (G)$ .

1.1F2F3

The evaluation map $Φ : L^{1} (G) \to ⨁_{π \in \hat{G}} End (H_{π})$ , $f \mapsto (π (f))_{π \in \hat{G}}$ , is injective and $*$ -multiplicative. It is $*$ -multiplicative by [F3]; for injectivity suppose $π (f) = 0$ for every $π \in \hat{G}$ . Then every matrix element $⟨ π (f) e_{j}, e_{i} ⟩$ vanishes, and these are $(1 / \sqrt{d_{π}}) \int_{G} f (g) u_{j i}^{π} (g) d μ (g)$ , the inner products of $f$ with $\overline{u_{j i}^{π}}$ up to nonzero constants. Conjugation sends the complete orthonormal family of [F2] to another complete orthonormal family: it preserves norms and turns each inner product into its conjugate. Hence vanishing of all these inner products forces $f = 0$ .

2.1F2step 1.1

$Φ$ is bijective. It is injective by step 1.1, $\dim L^{1} (G) = ∣ G ∣$ for the finite group, and the orthonormal basis of [F2] is indexed by the triples $(π, i, j)$ , so $\sum_{π \in \hat{G}} d_{π}^{2} = ∣ G ∣ = \dim L^{2} (G)$ [F2]; hence the two finite-dimensional spaces have equal dimension and $Φ$ is a linear isomorphism. Consequently $Φ$ is a $*$ -isomorphism of $L^{1} (G)$ onto the finite-dimensional C*-algebra $⨁_{π \in \hat{G}} End (H_{π})$ , and it is isometric for the transported norm $∥ f ∥_{Φ} : = ∥ Φ (f) ∥ = \max_{π \in \hat{G}} ∥ π (f) ∥$ .

3.1F1F2F4step 2.1

The full and reduced norms coincide on $L^{1} (G)$ . By [F4] $∥ f ∥_{C^{*}} = \sup_{ρ} ∥ ρ (f) ∥$ over all unitary representations $ρ$ ; by [F1] each $ρ$ is a discrete direct sum ${⨁^{^}}_{i} σ_{i}$ of irreducibles, so $∥ ρ (f) ∥ = \sup_{i} ∥ σ_{i} (f) ∥$ and therefore $\sup_{ρ} ∥ ρ (f) ∥ = \max_{π \in \hat{G}} ∥ π (f) ∥ = ∥ f ∥_{Φ}$ . By [F2] $λ ≅ {⨁^{^}}_{π} d_{π} π$ , so also $∥ λ (f) ∥ = \max_{π} ∥ π (f) ∥ = ∥ f ∥_{Φ}$ ; as $C_{r}^{*} (G)$ is the completion of $λ (L^{1} (G))$ , its norm on $L^{1} (G)$ is $∥ f ∥_{Φ}$ as well.

4.1F4F5F6step 3.1

The canonical surjection $C^{*} (G) ↠ C_{r}^{*} (G)$ of [F4] is isometric on the dense image of $L^{1} (G)$ by step 3.1, hence is injective on a dense subspace and therefore an isometric isomorphism of C*-algebras; both algebras are the completion of $L^{1} (G)$ in the common norm $∥ \cdot ∥_{Φ}$ . That completion is $L^{1} (G)$ itself, because step 2.1 exhibits it as isometric to the finite-dimensional, hence complete, algebra $⨁_{π} End (H_{π})$ . Therefore $C^{*} (G) = C_{r}^{*} (G) ≅ ⨁_{π \in \hat{G}} End (H_{π}) ≅ ⨁_{π \in \hat{G}} M_{d_{π}} (C)$ by [F5], a finite-dimensional algebra with one matrix block per irreducible class. It is semisimple by [F6]: the regular module of $M_{d} (C)$ is the direct sum of its column left ideals, each simple because matrix units send any nonzero column vector to every coordinate vector. The central block projections give the corresponding direct sum for the finite product of matrix algebras.

5.1given∎

The Axiom of Choice is inherited from the Peter-Weyl decomposition, the representation correspondence and the group C*-algebra constructions; the dimension count and the norm comparison add no further choice (The Axiom of Choice).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

76 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)