Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 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.

Q(ζ3,23,33) is a Kummer extension with quotient (Z/3)2

Example

Let F=Q(ζ3) and

K=F(23,33).

Then K/F is a Kummer extension, and the subgroup generated by the classes of 2 and 3 in F×/(F×)3 is isomorphic to (Z/3)2. Consequently

Gal⁡(K/F)≅(Z/3)2.

Facts & Assumptions

Given: The field F=Q(ζ3) and the extension K=F(23,33).

[L1]

Kummer theory identifies finite abelian extensions of exponent dividing 3 with subgroups of F×/(F×)3 (Kummer theory classifies finite abelian extensions of exponent dividing n by subgroups between (F×)n and F×).

[L2]

Norm and trace are given by the embedding formulas (Norm and trace from embeddings, with the inseparable exponent in the norm formula).

Verification

technique · direct
1.1L2algebra

The field F contains μ3, so adjoining cube roots is exactly the Kummer situation of [L1]. To show that the classes of 2 and 3 are independent modulo cubes, suppose 2a3b=c3in F×. Taking norms from F to Q gives 22a32b=NF/Q(c)3. The left side is a rational cube only when 3∣2a and 3∣2b, hence only when 3∣a and 3∣b. Therefore the classes of 2 and 3 each have order 3 and generate a subgroup isomorphic to (Z/3)2.

2.1L1step 1.1∎

By [L1], the field generated by the corresponding cube roots is a Kummer extension with Galois group Hom⁡((Z/3)2,μ3)≅(Z/3)2. Since K is exactly that field, the stated conclusion follows.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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