Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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)×B/(F×)n→μn is perfect

Statement

Let F be a field, let n≥1, assume char⁡F∤n, and assume μn⊆F. Let

(F×)n⊆B⊆F×

have finite quotient, and let K=F(B1/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×)n⟩:=σ(β)β,βn=b,

defines a well-defined bilinear pairing

Gal⁡(K/F)×B/(F×)n→μ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(B1/n), an automorphism σ∈Gal⁡(K/F), and an element b∈B with chosen n-th root β∈K.

[F1]

A Kummer extension is a finite Galois extension generated by n-th roots of elements of B, with μn⊆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.1F1algebra

Because σ(β)n=σ(b)=b=βn, the quotient σ(β)/β is an n-th root of unity, so it lies in μn⊆F. If β′=ζβ is another chosen n-th root of b, then σ(β′)β′=σ(ζ)σ(β)ζβ=σ(β)β, since σ fixes F and hence ζ. If b′=bcn represents the same class in B/(F×)n, then choosing β′=βc gives the same quotient. Thus the pairing is well defined.

2.1step 1.1algebra

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

2.2F1step 1.1

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

2.3F1L1step 1.1

For nondegeneracy on the B/(F×)n side, let bˉ be nontrivial. Then β∉F, for otherwise b=βn would lie in (F×)n. By [F1] and [L1], some σ∈Gal⁡(K/F) satisfies σ(β)≠β. Hence ⟨σ,bˉ⟩=σ(β)β≠1, so no nontrivial class lies in the right kernel.

3.1step 1.1step 2.1step 2.2step 2.3∎

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

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