TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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.

The Kummer pairing $Gal (K / F) \times B / (F^{\times})^{n} \to μ_{n}$ is perfect

Statement

Let $F$ be a field, let $n \geq 1$ , assume $char F ∤ n$ , and assume $μ_{n} \subseteq F$ . Let

$(F^{\times})^{n} \subseteq B \subseteq F^{\times}$

have finite quotient, and let $K = F (B^{1 / n})$ be the associated finite Kummer extension (Kummer extensions from adjoining $n$ -th roots over a base field containing $μ_{n}$ ). Then the rule

$⟨ σ, b (F^{\times})^{n} ⟩ : = \frac{σ (β)}{β}, β^{n} = b,$

defines a well-defined bilinear pairing

$Gal (K / F) \times B / (F^{\times})^{n} \to μ_{n},$

and it is nondegenerate in both variables. In this sense the Kummer pairing is perfect.

Facts & Assumptions

Given: The field $F$ , the integer $n$ , the subgroup $B$ , the Kummer extension $K = F (B^{1 / n})$ , an automorphism $σ \in Gal (K / F)$ , and an element $b \in B$ with chosen $n$ -th root $β \in K$ .

[F1]

A Kummer extension is a finite Galois extension generated by $n$ -th roots of elements of $B$ , with $μ_{n} \subseteq F$ (Kummer extensions from adjoining $n$ -th roots over a base field containing $μ_{n}$ ).

[L1]

For a finite Galois extension, the fixed field of the full Galois group is the base field (Equivalent characterizations of a finite Galois extension).

Proof

technique · direct

1.1

Because $σ (β)^{n} = σ (b) = b = β^{n}$ , the quotient $σ (β) / β$ is an $n$ -th root of unity, so it lies in $μ_{n} \subseteq F$ . If $β^{'} = ζ β$ is another chosen $n$ -th root of $b$ , then $\frac{σ (β^{'})}{β^{'}} = \frac{σ (ζ) σ (β)}{ζ β} = \frac{σ (β)}{β},$ since $σ$ fixes $F$ and hence $ζ$ . If $b^{'} = b c^{n}$ represents the same class in $B / (F^{\times})^{n}$ , then choosing $β^{'} = β c$ gives the same quotient. Thus the pairing is well defined.

F1algebra

2.1

Bilinearity is immediate: $⟨ σ τ, \overset{ˉ}{b} ⟩ = \frac{σ τ (β)}{β} = \frac{σ (τ (β))}{τ (β)} \frac{τ (β)}{β} = ⟨ σ, \overset{ˉ}{b} ⟩ ⟨ τ, \overset{ˉ}{b} ⟩,$ and for classes $\overset{ˉ}{b}, \overset{ˉ}{c}$ represented by roots $β, γ$ , $⟨ σ, \overset{ˉ}{b} \overset{ˉ}{c} ⟩ = \frac{σ (β γ)}{β γ} = \frac{σ (β)}{β} \frac{σ (γ)}{γ} = ⟨ σ, \overset{ˉ}{b} ⟩ ⟨ σ, \overset{ˉ}{c} ⟩ .$

step 1.1algebra

2.2

For nondegeneracy on the Galois side, let $σ \neq 1$ . Since $K$ is generated over $F$ by the chosen $n$ -th roots of elements of $B$ , some such root $β$ satisfies $σ (β) \neq β$ . For the class $\overset{ˉ}{b}$ of $b = β^{n}$ , one then has $⟨ σ, \overset{ˉ}{b} ⟩ = \frac{σ (β)}{β} \neq 1.$ So no nontrivial automorphism lies in the left kernel.

F1step 1.1

2.3

For nondegeneracy on the $B / (F^{\times})^{n}$ side, let $\overset{ˉ}{b}$ be nontrivial. Then $β \notin F$ , for otherwise $b = β^{n}$ would lie in $(F^{\times})^{n}$ . By [F1] and [L1], some $σ \in Gal (K / F)$ satisfies $σ (β) \neq β$ . Hence $⟨ σ, \overset{ˉ}{b} ⟩ = \frac{σ (β)}{β} \neq 1,$ so no nontrivial class lies in the right kernel.

F1L1step 1.1

3.1

Steps 1.1, 2.1, 2.2, and 2.3 prove the stated well-defined bilinear pairing and its nondegeneracy in both variables.

step 1.1step 2.1step 2.2step 2.3∎

Depends on

Used by

Dependency tree · two levels

20 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

J. S. Milne, Fields and Galois Theory, v5.10, Remark 5.32 (standard reference, not scraped)
B. Conrad, Kummer Theory, Theorem 5.12 (standard reference, not scraped)

The Kummer pairing Gal⁡(K/F)×B/(F×)n→μnGal(K/F)×B/(F×)n→μn​ is perfect