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 fixed field of a group of field automorphisms
Definition
Let be a field and let be a subgroup of its automorphism group. The fixed field of is
This is a subfield of . Every field automorphism fixes and , so these elements lie in . If and , then and ; if also , then . Thus is closed under subtraction, multiplication, and inverses of nonzero elements. In particular, when (Relative field automorphisms and ), one has .
Depends on
Used by
- For a finite extension, |Aut(K/F)| divides [K:F] Corollary
- A finite normal extension is separable over its purely inseparable fixed field Lemma
- Artin's fixed-field lower bound [K:K^G]≥ |G| Lemma
- Artin's fixed-field upper bound [K:K^G]≤ |G| Lemma
- The character field is the stabilizer fixed field Lemma
- The elements of a finite extension fixed by the q-power map are exactly the base field Lemma
- A finite extension of a finite field of order q is Galois with cyclic Galois group generated by x↦ x^q Theorem
- Artin's fixed-field theorem: [K:K^G]=|G| and Aut(K/K^G)=G Theorem
- Polynomial algebras over fields have finite integral closures Theorem
- The intermediate fields of F_qⁿ/F_q are the F_qᵈ, one for each positive divisor d of n Theorem
Dependency tree · two levels
2 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, Section 3 (standard reference, not scraped)
- K. Conrad, The Galois Correspondence, Sections 4-5 (standard reference, not scraped)