Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

A degree-three Galois extension of Q inside Q(ζ7)

Example

Let ζ:=ζ7. Then the fixed field of the unique order-two subgroup of Gal(Q(ζ)/Q) is

Q(ζ+ζ1),

a degree-three Galois extension of Q with cyclic Galois group, and the element ζ+ζ1 has minimal polynomial

t3+t22t1.

Facts & Assumptions

Given: A primitive seventh root of unity ζ=ζ7.

[L1]

Gal(Q(ζ7)/Q)(Z/7)× and has order φ(7)=6 ([Q(ζn):Q]=φ(n) and Gal(Q(μn)/Q)(Z/n)×).

[L2]

A finite cyclic group has exactly one subgroup of each order dividing its own (A finite cyclic group has exactly one subgroup of each order dividing its own).

[L3]

For a finite Galois extension, subgroups correspond to intermediate fields, and the fixed field of a subgroup H has degree equal to the subgroup index (The fundamental theorem of finite Galois theory).

[L4]

Every finite subgroup of the unit group of an integral domain is cyclic (Every finite subgroup of the unit group of an integral domain is cyclic).

[L5]

Under the finite Galois correspondence, a normal subgroup H has a Galois fixed field and restriction gives Gal(F/Q)G/H (Normal subgroups, conjugate fields, and quotient groups in the Galois correspondence).

Verification

technique · direct
1.1

By [L1] the Galois group of Q(ζ)/Q is isomorphic to the finite subgroup (Z/7)× of the unit group of the field Z/7, so [L4] makes it cyclic; its order is 6. Thus [L2] gives a unique subgroup H of order 2, and [L3] makes its fixed field F have degree [F:Q]=6/2=3.

L1L2L3L4
2.1

The subgroup H is generated by the class [1], so it acts by complex conjugation. Therefore ζ+ζ1 is fixed by H and lies in F.

step 1.1algebra
3.1

Put x:=ζ+ζ1. Then ζ2+ζ2=x22,ζ3+ζ3=x33x. Since 1+ζ+ζ2+ζ3+ζ4+ζ5+ζ6=0, dividing by ζ3 gives 1+(ζ+ζ1)+(ζ2+ζ2)+(ζ3+ζ3)=0. Substituting the expressions above yields x3+x22x1=0.

step 2.1algebra
4.1

The element x is not rational: if it were, then ζ would satisfy the quadratic polynomial t2xt+1Q[t], which would force [Q(ζ):Q]2, contradicting [L1]. Since xF, the prime degree [F:Q]=3 from step 1.1 leaves only the subfields Q and F, so Q(x)=F. Therefore the minimal polynomial of x has degree 3, and the cubic from step 3.1 is that minimal polynomial.

step 1.1step 3.1L1
5.1

The ambient Galois group is cyclic and hence abelian, so H is normal. By [L5], the fixed field F/Q is Galois and Gal(F/Q) is isomorphic to the quotient by H, which has order 3. The group is cyclic by [L6], so F/Q is a cyclic cubic Galois extension.

step 1.1L5L6algebra

Remarks

  • This is the smallest nontrivial case of the subfield theorem. The subgroup lattice of (Z/7)× has one index-two subgroup, and the fixed field is already visible through the real element ζ+ζ1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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