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

Characters of a finite product factor coordinatewise

Statement

Let $G_{1}, \dots, G_{r}$ be finite abelian groups and let $P = G_{1} \times \dots \times G_{r}$ be their recursively parenthesized external direct product. By convention, $P$ is the trivial group when $r = 0$ . Restriction to the coordinate factors gives a bijection $\hat{P} ⟶ \hat{G_{1}} \times \dots \times \hat{G_{r}} .$ Its inverse sends $(χ_{1}, \dots, χ_{r})$ to $χ (g_{1}, \dots, g_{r}) = \prod_{i = 1}^{r} χ_{i} (g_{i})$ . For $r = 0$ , both sides are singletons.

Facts & Assumptions

Given: A finite list of finite abelian groups with the coordinatewise operation on its iterated product.

[F1]

An additive character is a group homomorphism to $C^{\times}$ ; it preserves addition and sends the identity to $1$ (Additive characters of a finite abelian group).

[F2]

The external direct product has carrier $G \times H$ and componentwise operation (The external direct product $G \times H$ with componentwise multiplication).

[F3]

This componentwise operation makes $G \times H$ a group ( $G \times H$ is a group with identity $(e_{G}, e_{H})$ , coordinatewise inverses, and homomorphic coordinate projections).

[F4]

The dual $\hat{P}$ is the set of additive characters of $P$ (Dual group of a finite abelian group).

Proof

1.1F1F2F4givenconstruct

For $χ \in \hat{P}$ as defined in [F4], put $χ_{i} (g_{i}) : = χ (0, \dots, 0, g_{i}, 0, \dots, 0)$ . The coordinate embedding preserves addition by the componentwise operation in [F2], so [F1] shows each $χ_{i}$ is a character.

1.2F1F2givenconstruct

For a tuple $(χ_{i})$ , define $σ ((χ_{i})) (g_{1}, \dots, g_{r}) : = \prod_{i} χ_{i} (g_{i})$ . The componentwise operation and each homomorphism law give $σ ((χ_{i})) (g + h) = σ ((χ_{i})) (g) σ ((χ_{i})) (h)$ , so this is a character of $P$ .

2.1step 1.2F1F2

Restricting $σ ((χ_{i}))$ to the $i$ th coordinate gives $χ_{i}$ , because all other coordinates are zero and every character takes the identity to $1$ . Thus restriction after $σ$ is the identity on the product of duals.

2.2step 1.1F1F2F3algebra

Every $(g_{1}, \dots, g_{r})$ is the sum of its coordinate vectors. Applying a homomorphism $χ$ to this sum gives $χ (g_{1}, \dots, g_{r}) = \prod_{i} χ_{i} (g_{i})$ , so $σ$ after restriction is the identity on $\hat{P}$ . For $r = 0$ , the sole group element and sole character give the stated singleton bijection.

3.1F4step 2.1step 2.2∎

Steps 2.1 and 2.2 show the two displayed maps are inverse bijections between the character sets in [F4], including the empty-product case.

Depends on

Used by

Dependency tree · two levels

11 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

Ronald de Wolf, Quantum Computing: Lecture Notes, version 6 (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (standard reference, not scraped)
John Preskill, Quantum Information, Chapter 6: Quantum Algorithms (standard reference, not scraped)