TheoremStatement: 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.

Finite abelian group is canonically isomorphic to its double dual

Statement

For a finite abelian group $G$ , give $\hat{G}$ its pointwise multiplication. Its dual $\hat{\hat{G}}$ consists of functions $Φ : \hat{G} \to C^{\times}$ satisfying $Φ (χ ψ) = Φ (χ) Φ (ψ)$ . The evaluation map $ev : G ⟶ \hat{\hat{G}}, ev (g) (χ) : = χ (g),$ is a group isomorphism. The map itself is canonical; a decomposition into cyclic factors is used only to prove it is injective.

Facts & Assumptions

Given: A finite abelian group $G$ and its pointwise character dual.

[F1]

$\hat{G}$ is a finite abelian group under pointwise multiplication (Pointwise character dual is a finite abelian group).

[F2]

A finite abelian group and its dual have equal cardinality (A finite abelian group and its character dual have equal order).

[F3]

Every finite abelian group has an invariant-factor product decomposition (Fundamental theorem of finite abelian groups: invariant-factor form).

[F4]

Characters of a finite product factor coordinatewise (Characters of a finite product factor coordinatewise); on a cyclic factor $C_{n}$ , a character may take generator value $ω_{n} : = \exp (2 π i / ι_{R} (n))$ , whose powers $ω_{n}^{m}$ for $0 \leq m < n$ are distinct (A cyclic group of order n has exactly n additive characters, The $n$ -th roots of a complex number and the $n$ distinct roots of unity for every $n \geq 1$ ).

[F5]

If a subset $B$ of a finite set $A$ has $∣ B ∣ = ∣ A ∣$ , then $B = A$ (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ); finite cardinality is transported by bijections (The cardinality $∣ A ∣$ of a finite set).

[F6]

A group isomorphism is a bijective group homomorphism (Group isomorphisms, automorphisms and the set $Aut (G)$ ).

[F7]

$\hat{G}$ is the set of additive characters with pointwise multiplication; its elements satisfy $χ (g + h) = χ (g) χ (h)$ (Dual group of a finite abelian group).

[F8]

An additive character satisfies $χ (- h) = χ (h)^{- 1}$ (Additive characters of a finite abelian group).

Proof

1.1F1F7givenconstruct

For each $g \in G$ , evaluation on the dual group [F7] is a character: if $χ, ψ \in \hat{G}$ , then $ev (g) (χ ψ) = χ (g) ψ (g) = ev (g) (χ) ev (g) (ψ)$ . Thus $ev (g) \in \hat{\hat{G}}$ .

1.2F3F4givenconstruct

If $G$ is nontrivial, fix the isomorphism $φ : G \to \prod_{i} C_{n_{i}}$ from [F3]. For any nonzero $g$ , some coordinate is $φ (g)_{j} = [m]$ with $1 \leq m < n_{j}$ . In the product, the character trivial on every coordinate except $j$ , with generator value $ω_{n_{j}}$ on that factor, exists by [F4]. Its composite $χ$ with $φ$ is a character of $G$ and satisfies $χ (g) = ω_{n_{j}}^{m} \neq 1$ , because the listed $n_{j}$ roots are distinct and $m$ is nonzero modulo $n_{j}$ . Thus every nonzero element is detected by a character. The trivial-group case has no nonzero element and satisfies this statement vacuously.

2.1F1givenstep 1.1

Evaluation is a homomorphism from $G$ to the pointwise group $\hat{\hat{G}}$ , since for every $χ$ , $ev (g + h) (χ) = χ (g + h) = χ (g) χ (h) = (ev (g) ev (h)) (χ)$ .

2.2F7F8step 1.2given

If $ev (g) = ev (h)$ , then for every $χ \in \hat{G}$ , [F7] and [F8] give $χ (g - h) = χ (g) χ (h)^{- 1} = 1$ . If $g - h \neq 0$ , step 1.2 supplies a character with $χ (g - h) \neq 1$ , a contradiction. Hence $g = h$ and evaluation is injective.

3.1F1F2step 2.2

By [F2], $∣ \hat{G} ∣ = ∣ G ∣$ and, applying [F2] to the finite abelian group $\hat{G}$ from [F1], $∣ \hat{\hat{G}} ∣ = ∣ \hat{G} ∣$ . Thus the finite domain and codomain of the injective map in step 2.2 have equal cardinality.

4.1F5F6step 2.1step 3.1∎

The image of $ev$ is a subset of $\hat{\hat{G}}$ with the same finite cardinality as that codomain, because $ev$ is injective. By [F5] the image is the whole codomain, so $ev$ is bijective. Together with step 2.1 and the definition [F6], it is a group isomorphism.

Depends on

Used by

A Fourier sample cuts a larger common kernel Lemma
Double annihilator returns the subgroup Theorem

Dependency tree · two levels

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