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.

Double annihilator returns the subgroup

Statement

Let $G$ be a finite abelian group and $H \leq G$ . Under the canonical evaluation identification $G ≅ \hat{\hat{G}}$ , $(H^{⊥})^{⊥} = H .$

Facts & Assumptions

Given: A finite abelian group $G$ and subgroup $H \leq G$ .

[F1]

Evaluation identifies $G$ isomorphically with $\hat{\hat{G}}$ (Finite abelian group is canonically isomorphic to its double dual).

[F2]

For $K \leq \hat{G}$ , its annihilator in $G$ is $K^{⊥} = {g \in G : χ (g) = 1 for every χ \in K}$ (Character annihilator of a subgroup).

[F3]

The dual $\hat{G}$ is a finite abelian group of cardinality $∣ G ∣$ (Pointwise character dual is a finite abelian group), and annihilators of subgroups are subgroups (Annihilators of subgroups are subgroups).

[F4]

For a finite abelian group $K$ and subgroup $L \leq K$ , its character annihilator $L^{⊥_{K}} : = {Φ \in \hat{K} : Φ (ℓ) = 1 for all ℓ \in L}$ satisfies $∣ L^{⊥_{K}} ∣ ∣ L ∣ = ∣ K ∣$ (Subgroup-annihilator cardinality).

[F5]

A subset of a finite set with the same cardinality as the whole set equals the whole set (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ).

[F6]

A subgroup contains the identity and is nonempty, so its cardinality is positive (Subgroup).

Proof

1.1F1F2givenconstruct

Put $A : = (H^{⊥})^{⊥_{\hat{G}}} = {Φ \in \hat{\hat{G}} : Φ (χ) = 1 for every χ \in H^{⊥}}$ , the character annihilator of the subgroup $H^{⊥}$ inside the group $\hat{G}$ . If $h \in H$ , every $χ \in H^{⊥}$ has $χ (h) = 1$ by [F2], so $ev (h) (χ) = 1$ for every such $χ$ and $ev (h) \in A$ . Thus $ev (H) \subseteq A$ .

2.1F1F3F4F5F6step 1.1algebra

By [F3], $H^{⊥}$ is a subgroup of the finite abelian group $\hat{G}$ ; [F6] gives $∣ H^{⊥} ∣ \geq 1$ . Applying [F4] to $G, H$ and then to $\hat{G}, H^{⊥}$ gives $∣ H^{⊥} ∣ ∣ H ∣ = ∣ G ∣$ and $∣ A ∣ ∣ H^{⊥} ∣ = ∣ \hat{G} ∣ = ∣ G ∣$ , the last equality following from [F3]. Cancellation gives $∣ A ∣ = ∣ H ∣$ . The injective evaluation isomorphism [F1] gives $∣ ev (H) ∣ = ∣ H ∣$ ; with step 1.1, the finite-subset result [F5] yields $A = ev (H)$ .

3.1F1F2step 2.1∎

By definition [F2], $g \in (H^{⊥})^{⊥}$ exactly when $χ (g) = 1$ for every $χ \in H^{⊥}$ , which is exactly when $ev (g) \in A$ . Since step 2.1 proves $A = ev (H)$ and [F1] makes evaluation injective, its preimage is $H$ ; hence $(H^{⊥})^{⊥} = H$ .

Depends on

Used by

A Fourier sample cuts a larger common kernel Lemma

Dependency tree · two levels

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