Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + 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.

K(μn)/K is Galois and σaσ embeds its Galois group into (Z/n)×

Statement

Let K be a field and n1 with charKn (The characteristic of a ring: the least n1 with n1R=0 when one exists, and 0 otherwise), and let E=K(μn) (The cyclotomic extension K(μn) as a splitting field of tn1). Then E/K is a finite Galois extension, and there is an injective group homomorphism

Gal(E/K)(Z/n)×,σ[aσ]n,

where aσ is any integer with σ(ζ)=ζaσ for a primitive n-th root of unity ζE. The class [aσ]n does not depend on which primitive n-th root of unity is used, and σ(x)=xaσ holds for every xμn(E).

Facts & Assumptions

Given: A field K, an integer n1 with charKn, the extension E=K(μn) (The cyclotomic extension K(μn) as a splitting field of tn1), and a primitive n-th root of unity ζE (The group μn(K) of n-th roots of unity in a field, and primitive n-th roots of unity).

[L1]

For n1, tn1 is separable over K when charKn; in a splitting field E the group μn(E) is then cyclic of order n, has φ(n) primitive n-th roots of unity, and E=K(ζ) for every primitive n-th root of unity ζE (tn1 is separable over K exactly when the characteristic does not divide n, and then a splitting field carries n distinct n-th roots of unity).

[L2]

For a finite extension L/F with G=Aut(L/F), the conditions "L/F is Galois", "L is the splitting field over F of a separable polynomial", "G=[L:F]" and "LG=F" are equivalent (Equivalent characterizations of a finite Galois extension, Finite Galois extensions and Gal(K/F), Relative field automorphisms and Aut(K/F)).

[L3]

μn(E) is a finite cyclic subgroup of E× of order dividing n, and when its order is n its generators are exactly the primitive n-th roots of unity (μn(K) is cyclic of order dividing n, and has a primitive n-th root of unity exactly when its order is n).

[L4]

In a cyclic group g of finite order m, ga generates the group if and only if gcd(a,m)=1 (A cyclic group of order n has exactly φ(n) generators).

[L6]

For n1 and aZ, the class [a]nZ/n (The congruence class [a]n and the quotient set Z/n) is a unit of Z/n if and only if gcd(a,n)=1 (For n1, [a]n is a unit if and only if gcd(a,n)=1); the units form the group (Z/n)× of order φ(n) (The unit group (Z/n)× and Euler's totient φ(n)=(Z/n)× for n1).

[L7]

If a is algebraic over a field K, then the simple extension K(a)/K is finite, with degree equal to the degree of the minimal polynomial of a (A simple algebraic extension is its minimal-polynomial quotient and has power basis 1,a,,an1 and degree n).

Proof

technique · direct
1.1

By [L1] the polynomial tn1 is separable over K, the group μn(E) is cyclic of order n generated by ζ, and E=K(ζ). The element ζ is algebraic because it is a root of tn1, so [L7] makes E/K finite. Since E is the splitting field of the separable polynomial tn1, [L2] now makes E/K finite Galois.

L1L2L3L7given
2.1

Each σGal(E/K) maps μn(E) into itself, since σ(x)n=σ(xn)=σ(1)=1; being injective on the finite set μn(E) it restricts to a bijection, and it is multiplicative, so it restricts to a group automorphism of μn(E).

step 1.1given
3.1

Hence σ(ζ) generates μn(E)=ζ, so σ(ζ)=ζa for some integer a, and [L4] gives gcd(a,n)=1, so [a]n(Z/n)× by [L6]. The class is well defined: ζa=ζb means ζab=1, which by [L5] and ord(ζ)=n says nab, that is [a]n=[b]n. Write [aσ]n for this class.

step 1.1step 2.1L4L5L6
4.1

For every xμn(E) one has x=ζj for some j, so σ(x)=σ(ζ)j=ζaσj=xaσ.

step 1.1step 3.1
4.2

The map σ[aσ]n is a group homomorphism: (στ)(ζ)=σ(ζaτ)=σ(ζ)aτ=ζaσaτ, so [aστ]n=[aσ]n[aτ]n by the well-definedness of step 3.1.

step 3.1L6
4.3

It is injective: if [aσ]n=[1]n then σ(ζ)=ζ by step 3.1, and since E=K(ζ) and σ fixes K pointwise, σ is the identity on E.

step 1.1step 3.1
5.1

The class is independent of the chosen primitive n-th root of unity: any other one is a generator ζ of μn(E) by [L3], so ζ=ζb for some b, and σ(ζ)=σ(ζ)b=ζaσb=(ζb)aσ=(ζ)aσ, which exhibits the same exponent class. With steps 4.1, 4.2 and 4.3 this proves the theorem.

step 1.1step 3.1step 4.1step 4.2step 4.3L3

Remarks

Depends on

Used by

Dependency tree · two levels

89 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