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 finite normal extension is separable over its purely inseparable fixed field
Statement
Let be a finite normal field extension and let be the fixed field of its -automorphisms. Then is finite purely inseparable and is finite Galois, hence in particular separable. If has characteristic zero, then . The argument uses only finite groups, finite root sets and finite generating lists, so it is choice-free.
Facts & Assumptions
Given: a finite normal extension , with and fixed field .
A finite extension has finite degree , a finite-dimensional vector space has a finite basis, and for the finitely many basis elements (The degree of a finite field extension, Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis, Finitely generated field extensions , Field extensions, generated subrings , generated subfields , and simple extensions).
For algebraic over a field there is a unique monic irreducible minimal polynomial , and exactly when (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).
A nonzero polynomial of degree over an integral domain has at most roots in that domain (A nonzero polynomial of degree over an integral domain has at most distinct roots).
is a group of -automorphisms of and is the subfield of -fixed elements, with (Relative field automorphisms and , The fixed field of a group of field automorphisms).
If is a finite group of automorphisms of a field , then (Artin's fixed-field lower bound ) and (Artin's fixed-field upper bound ).
is normal exactly when the minimal polynomial over of every splits over (A normal algebraic extension is one in which every minimal polynomial with a root in the extension splits there, Polynomials that split and splitting fields of a polynomial or a family of polynomials).
is separable over when it is algebraic over with separable minimal polynomial, and is separable when every element is separable; a polynomial is separable when it has no repeated root in a splitting field (Separable algebraic elements and separable extensions, Repeated roots in extension fields and separable polynomials). A finite extension is Galois when it is normal and separable (Finite Galois extensions and ).
A finite extension is algebraic, and in a tower of finite extensions degrees multiply (Every finite field extension is algebraic, Tower law for finite extensions: , Algebraic and transcendental elements and algebraic extensions).
If is normal with and is the minimal polynomial of over , then is a splitting field over of (A normal extension generated by finitely many elements is the splitting field of the product of their minimal polynomials).
If is a field isomorphism, and , are splitting fields of and , then extends to an isomorphism (A base-field isomorphism extends to an isomorphism between splitting fields of corresponding polynomials).
In characteristic every nonconstant irreducible is uniquely with irreducible, separable and maximal (In characteristic , every irreducible polynomial is uniquely with irreducible and separable); in characteristic zero every irreducible polynomial is separable, because an irreducible polynomial is separable exactly when its derivative is nonzero and the derivative of a nonconstant polynomial of characteristic zero does not vanish (An irreducible polynomial over a field is separable exactly when its derivative is nonzero, Repeated roots in extension fields and separable polynomials).
In a field of characteristic the map is injective (Frobenius is an injective endomorphism in characteristic , and an automorphism for finite fields), and a finite extension in characteristic is purely inseparable when every element satisfies for some (Purely inseparable algebraic extensions).
If is algebraic over with minimal polynomial of degree , then consists of the elements and is isomorphic to (A simple algebraic extension is its minimal-polynomial quotient and has power basis and degree ).
Proof
Proof technique: direct. 1.1 The group is finite. By [L1] choose with ; by [L8] and [L2] each has a minimal polynomial over . Every fixes and is a field homomorphism, so it is determined by the images , since these generate over ; and is a root of , because applying to gives as fixes the coefficients of . By [L3] the polynomial has at most roots in , so the map injects into the finite product of these root sets; hence is finite. [L1, L2, L3, L8, construct]
The fixed field satisfies by [L4], and : both bounds and hold by [L5], applied to the finite group of automorphisms of . In particular is a finite extension of degree .
The extension is finite Galois. It is finite by step 2.1. For let be its finite -orbit and put , a monic polynomial of degree with whose roots in are the distinct elements of the orbit. Every permutes , hence fixes the coefficients of , which are the elementary symmetric functions of the orbit; those coefficients therefore lie in , that is . It follows that the minimal polynomial of over , whose existence and divisibility property are given by [L2], divides in ; being a divisor of a polynomial that is a product of distinct linear factors, itself is a product of distinct linear factors over . Thus the minimal polynomial over of every splits over with distinct roots, so is normal by [L6] and separable by [L7]. Therefore is finite Galois by [L7].
The extension is purely inseparable, and in characteristic zero. Since is finite it is algebraic by [L8], and by [L1] and [L9] is a splitting field over of the product of the minimal polynomials of a finite generating list of . Let with minimal polynomial over , and let be any root of . The assignment defines an isomorphism of -extensions: the -algebra map with kills and so factors through by [L13], and it is injective because is a field. Moreover is a splitting field of over both and , since all roots of the lie in and generate it over , hence also over each of these intermediate fields. By [L10] applied over the base field the isomorphism extends to an isomorphism , which is an -automorphism because it fixes ; so for this , since lies in the fixed field . Hence has exactly one distinct root in , and by normality of it has all its roots in by [L6]. If has characteristic , write as in [L11] with irreducible and separable; the distinct roots of in correspond bijectively to the roots of in , because is injective by [L12], so has exactly one root and ; writing with gives and hence . Thus every element of has a -power in , so is purely inseparable by [L12]. If instead has characteristic zero, then the irreducible is separable by [L11], so has distinct roots in by [L7]; having exactly one root forces and . Hence in characteristic zero. This proves all three clauses of the statement.
Depends on
A normal algebraic extension is one in which every minimal polynomial with a root in the extension splits there
The fixed field of a group of field automorphisms
Relative field automorphisms and
Artin's fixed-field lower bound
Artin's fixed-field upper bound
A normal extension generated by finitely many elements is the splitting field of the product of their minimal polynomials
A base-field isomorphism extends to an isomorphism between splitting fields of corresponding polynomials
In characteristic , every irreducible polynomial is uniquely with irreducible and separable
An irreducible polynomial over a field is separable exactly when its derivative is nonzero
Purely inseparable algebraic extensions
Separable algebraic elements and separable extensions
Repeated roots in extension fields and separable polynomials
Finite Galois extensions and
The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element
A nonzero polynomial of degree over an integral domain has at most distinct roots
Every finite field extension is algebraic
The degree of a finite field extension
Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis
Finitely generated field extensions
Field extensions, generated subrings , generated subfields , and simple extensions
Polynomials that split and splitting fields of a polynomial or a family of polynomials
Algebraic and transcendental elements and algebraic extensions
Frobenius is an injective endomorphism in characteristic , and an automorphism for finite fields
A simple algebraic extension is its minimal-polynomial quotient and has power basis and degree
Tower law for finite extensions: