LemmaStatement: AI-adaptedProof: Literature-sourcedPipeline-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.

Continuous finite-dimensional representations of a product of finite groups factor through a finite subproduct

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $(G_{i})_{i \in I}$ be finite discrete groups, let $K : = \prod_{i \in I} G_{i}$ carry the product topology, and for a finite $F \subseteq I$ let $p_{F} : K \to K_{F} : = \prod_{i \in F} G_{i}$ be the coordinate projection. Then $K$ is a profinite group (it is the inverse limit of the finite groups $K_{F}$ over the directed set of finite subsets $F \subseteq I$ ), and for every continuous finite-dimensional unitary representation $ρ$ of $K$ there is a finite $F \subseteq I$ and a representation $ρ_{F}$ of the finite group $K_{F}$ with $ρ = ρ_{F} \circ p_{F}$ . Moreover the open normal subgroup $\ker p_{F}$ (the subgroup of tuples trivial in the $F$ -coordinates, canonically isomorphic to $\prod_{i \notin F} G_{i}$ ) can be chosen inside any prescribed identity neighbourhood, and every matrix coefficient of $ρ$ depends on the coordinates in $F$ only.

Facts & Assumptions

[F1]

The concrete inverse limit of the finite discrete groups $K_{F}$ over the directed set of finite subsets $F \subseteq I$ is the group of compatible tuples, equipped with the inverse limit topology, and it satisfies the universal property of the inverse limit; the coordinate projections are the maps $p_{F}$ . (The inverse limit is the set of compatible tuples in the Cartesian product, The inverse limit of finite groups carries the subspace topology from the product of discrete factors, The compatible-tuple construction satisfies the inverse-limit universal property in groups)

[F2]

A topological group topologically isomorphic to an inverse limit of finite discrete groups is profinite, and for such a presentation the kernels of the coordinate projections form an open normal neighbourhood basis at the identity. (A profinite group is a topological group isomorphic to an inverse limit of finite discrete groups, The kernels of the finite coordinate projections form an open normal neighbourhood basis at the identity)

[F3]

A continuous finite-dimensional unitary representation $ρ$ of a profinite group factors through a finite quotient: for the presentation $K = \underset{\leftarrow}{l i m} K_{F}$ there is a finite $F$ with $\ker p_{F} \subseteq \ker ρ$ , so $ρ = ρ_{F} \circ p_{F}$ for a representation $ρ_{F}$ of $K_{F}$ , and every matrix coefficient of $ρ$ factors through that finite quotient. (Continuous finite-dimensional representations of profinite groups factor through finite quotients)

[F4]

In the product topology on $\prod_{i \in I} G_{i}$ the basic identity neighbourhoods fix finitely many coordinates, each $p_{F}$ is continuous and surjective, and $\ker p_{F}$ is the closed subgroup of tuples trivial in the coordinates of $F$ , canonically isomorphic to $\prod_{i \notin F} G_{i}$ . (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space)

[F5]

Matrix coefficients are $c_{v, w}^{ρ} (k) = ⟨ ρ (k) v, w ⟩$ for vectors $v, w$ , and strong continuity of a finite-dimensional representation makes $k \mapsto ρ (k)$ norm-continuous. (Matrix coefficient of a unitary representation, Strongly continuous unitary representations, invariant linear subspaces and intertwiners)

[F6]

The first isomorphism theorem gives $K / \ker p_{F} ≅ p_{F} (K) = K_{F}$ . (First isomorphism theorem for groups: $G / \ker f ≅ im f$ )

Proof

Given: AC, Finite discrete groups $(G_{i})_{i \in I}$ , the product $K = \prod_{i} G_{i}$ with product topology, coordinate projections $p_{F}$ for finite $F \subseteq I$ , and a continuous finite-dimensional unitary representation $ρ$ of $K$ .

1.1F1F2F4F6

The map $x \mapsto (p_{F} (x))_{F}$ from $K$ to the set of compatible tuples is a topological group isomorphism onto ${\underset{\leftarrow}{l i m}}_{F} K_{F}$ , with inverse given by the compatible tuple's coordinates: it is a group homomorphism because each $p_{F}$ is, it is injective because the coordinates determine $x$ , it is surjective because the coordinates of a compatible tuple define an element of $K$ whose projections are the given ones, and both directions are continuous for the product and inverse-limit topologies by [F1]; hence $K$ is profinite by [F2], and the kernels $\ker p_{F}$ form an open normal neighbourhood basis at the identity. By [F4] each $\ker p_{F}$ is the closed subgroup of tuples trivial in the coordinates of $F$ and is canonically isomorphic to $\prod_{i \notin F} G_{i}$ ; moreover $p_{F}$ is surjective with $K / \ker p_{F} ≅ K_{F}$ by [F6].

2.1F3F5step 1.1∎

Apply the profinite factorisation lemma [F3] to the profinite presentation of $K$ as ${\underset{\leftarrow}{l i m}}_{F} K_{F}$ : there is a finite $F \subseteq I$ with $\ker p_{F} \subseteq \ker ρ$ , and $ρ$ factors as $ρ = ρ_{F} \circ p_{F}$ for a representation $ρ_{F}$ of the finite group $K_{F}$ ; since the $\ker p_{F}$ form an identity neighbourhood basis by step 1.1, the finite set $F$ may be chosen so that $\ker p_{F}$ lies inside any prescribed identity neighbourhood of $K$ . Every matrix coefficient $c_{v, w}^{ρ} (k) = ⟨ ρ_{F} (p_{F} (k)) v, w ⟩$ by [F5] depends only on $p_{F} (k)$ , hence only on the coordinates in $F$ , and is constant on the cosets of $\ker p_{F}$ ; this proves the lemma.

Depends on

Used by

Peter-Weyl for an infinite product of finite groups Example

Dependency tree · two levels

46 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

David A. Vogan, Review of Harmonic Analysis on Compact Groups (MIT lecture notes, 12 pp.) (standard reference, not scraped)
Constantin Teleman, Representation Theory (Berkeley lecture notes, 60 pp.) (standard reference, not scraped)