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.

Subgroup-annihilator cardinality

Statement

For a subgroup $H \leq G$ of a finite abelian group, descent and inflation identify $H^{⊥}$ with the character dual of $G / H$ . Consequently $∣ H^{⊥} ∣ = ∣ G / H ∣ = [G : H] = \frac{∣ G ∣}{∣ H ∣}, ∣ H^{⊥} ∣ ∣ H ∣ = ∣ G ∣ .$ The quotient convention is left cosets, with additive notation.

Facts & Assumptions

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

[F1]

Every subgroup of an abelian group is normal (Every subgroup of an abelian group is normal).

[F2]

The quotient $G / H$ consists of cosets with well-defined group operation, and its order is the index $[G : H]$ (The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ , For $N ⊴ G$ , the cosets form a group with identity $N$ and inverse $(g N)^{- 1} = g^{- 1} N$ , The coset set $G / H$ and the index $[G : H]$ of a subgroup).

[F3]

A quotient of an abelian group is abelian (Every quotient group of an abelian group is abelian).

[F4]

Cosets satisfy $g + H = g^{'} + H$ exactly when $g^{'} - g \in H$ ( $x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$ ).

[F5]

A finite abelian group $Q$ with an invariant-factor decomposition has $∣ \hat{Q} ∣ = ∣ Q ∣$ , including the empty decomposition of the trivial group (A finite abelian group and its character dual have equal order).

[F6]

Lagrange's theorem gives $∣ G ∣ = [G : H] ∣ H ∣$ for finite $G$ and subgroup $H$ (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[F7]

A subgroup contains the group identity, so $∣ H ∣ \geq 1$ (Subgroup).

[F8]

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

[F9]

$H^{⊥}$ consists exactly of the characters trivial on every element of $H$ (Character annihilator of a subgroup).

[F10]

Every finite abelian group has an invariant-factor decomposition; the trivial group corresponds to the empty list (Fundamental theorem of finite abelian groups: invariant-factor form).

Proof

1.1F1F2F3F6

By [F1] the quotient is defined; [F2] gives its group law, and [F3] makes $Q : = G / H$ finite abelian. Finiteness also follows from the finite coset partition in [F6].

1.2F2F3F8F9givenconstruct

Let $π : G \to Q$ be $π (g) = g + H$ . The quotient law in [F2] gives $π (g + g^{'}) = (g + H) + (g^{'} + H) = π (g) + π (g^{'})$ , so $π$ is a homomorphism. For $h \in H$ , $π (h) = H$ , the identity coset; every character sends the identity to $1$ . Thus for $ψ \in \hat{Q}$ , $ψ \circ π$ is a character by [F8] and is trivial on $H$ , so [F9] shows inflation maps $\hat{Q}$ into $H^{⊥}$ .

1.3F2F4F8construct

For $χ \in H^{⊥}$ , define $\tilde{χ} (g + H) : = χ (g)$ . If $g + H = g^{'} + H$ , [F4] gives $g^{'} - g \in H$ , hence $χ (g^{'}) = χ (g) χ (g^{'} - g) = χ (g)$ ; so $\tilde{χ}$ is well defined. For cosets $g + H, g^{'} + H$ , the quotient law [F2] gives $\tilde{χ} ((g + H) + (g^{'} + H)) = χ (g + g^{'}) = χ (g) χ (g^{'})$ , so $\tilde{χ}$ is a character of $Q$ .

2.1step 1.1step 1.2step 1.3F2F5F10

For every $g \in G$ , $(\tilde{χ} \circ π) (g) = \tilde{χ} (g + H) = χ (g)$ ; for every $ψ \in \hat{Q}$ and coset $g + H$ , descent of its inflation returns $\tilde{(ψ \circ π)} (g + H) = (ψ \circ π) (g) = ψ (g + H)$ . Thus inflation and descent are inverse bijections. Since $Q$ is finite abelian by step 1.1, [F10] supplies an invariant-factor decomposition of $Q$ , with the empty list allowed when $Q$ is trivial. Applying [F5] to this decomposition gives $∣ H^{⊥} ∣ = ∣ \hat{Q} ∣ = ∣ Q ∣$ , and by [F2], $∣ Q ∣ = [G : H]$ .

3.1step 2.1F6F7∎

Lagrange [F6] gives $∣ G ∣ = [G : H] ∣ H ∣$ . Combining with step 2.1 gives $∣ H^{⊥} ∣ ∣ H ∣ = ∣ G ∣$ , and division by the positive integer $∣ H ∣$ from [F7] gives $∣ H^{⊥} ∣ = ∣ G ∣ / ∣ H ∣$ .

Depends on

Used by

Double annihilator returns the subgroup Theorem
Fourier samples are uniform in the annihilator Theorem
Fourier transform of a subgroup coset indicator 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)