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.
If and , then a degree- extension is cyclic exactly when it is with and irreducible
Statement
Let be a field, let , assume , and assume contains a primitive -th root of unity. For a finite extension of degree , the following are equivalent:
- is cyclic.
- There exists such that , , and is irreducible over .
Facts & Assumptions
Given: A field , an integer , a primitive -th root of unity , and a finite extension of degree .
The Lagrange resolvent is (The Lagrange resolvent attached to a cyclic action and a root of unity).
Distinct characters are linearly independent (Dedekind's linear independence theorem for distinct characters).
If an extension contains one nonzero root of , then all roots are , and the splitting field is obtained by adjoining and the relevant roots of unity (After adjoining one nonzero root of , all roots are with ).
When , the polynomial is separable and a splitting field has cyclic root-of-unity group of order ( is separable over exactly when the characteristic does not divide , and then a splitting field carries distinct -th roots of unity).
A finite extension is Galois exactly when it is the splitting field of a separable polynomial (Equivalent characterizations of a finite Galois extension).
Embeddings of a simple algebraic extension correspond to the distinct roots of the minimal polynomial (-embeddings of into an algebraically closed field correspond to the distinct roots of ).
Proof
For the forward direction, assume is cyclic and choose a generator of . The distinct powers are distinct characters , so [L1] makes the resolvent operator of [F1] nonzero. Choose with .
For the converse direction, assume , , and is irreducible. If , then and the irreducible polynomial is , which forces . Hence , so the extension is cyclic. Assume from now on that . Then , and [L2] shows every root of is with . Because [L3] makes the roots of distinct, these roots are distinct as well. Hence all roots of already lie in , and the polynomial is separable, so is its splitting field and [L4] makes Galois.
In the nonzero case of step 1.2, the root of the irreducible polynomial determines, by [L5], an -embedding sending to , hence an automorphism of . Its powers send to , so has order . Because and a finite Galois extension has at most automorphisms, is cyclic of order .
Because the element is fixed by and hence by the whole cyclic Galois group, so . If and , then so , contradicting primitivity of . Therefore no smaller positive power of lies in . The minimal polynomial of divides and has degree , so it is exactly and .
Steps 2.2 and 2.1 prove the equivalence.
Remarks
- The irreducibility clause is what forces degree exactly . Without it, adjoining one -th root can produce a proper divisor of .
Depends on
- The Lagrange resolvent attached to a cyclic action and a root of unity
- Dedekind's linear independence theorem for distinct characters
- After adjoining one nonzero root $\alpha$ of $x^n-a$, all roots are $\zeta\alpha$ with $\zeta^n=1$
- $t^{n}-1$ 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
- Equivalent characterizations of a finite Galois extension
- $F$-embeddings of $F(\alpha)$ into an algebraically closed field correspond to the distinct roots of $m_{\alpha}$
- The degree $[K:F]=\dim_F K$ of a finite field extension
Used by
- Kummer extensions from adjoining n-th roots over a base field containing μₙ Definition
- Cardano's formula for x³-3x-1 from the Lagrange resolvent Example
- Over ℚ(ω), the splitting field of x³-2 is a cyclic cubic extension Example
- In characteristic 0, a polynomial solvable by radicals has a solvable Galois group Theorem
- In characteristic 0, a solvable Galois group makes a polynomial solvable by radicals Theorem
- Kummer theory classifies finite abelian extensions of exponent dividing n by subgroups between (F^×)ⁿ and F^× Theorem
- The Kummer pairing Gal(K/F)× B/(F^×)ⁿ→μₙ is perfect Theorem
Dependency tree · two levels
42 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, Proposition 5.27 (standard reference, not scraped)
- J. Ash, Basic Abstract Algebra, Section 6.7 (standard reference, not scraped)