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.
Norm and trace from embeddings, with the inseparable exponent in the norm formula
Statement
Let be a finite field extension, let be an algebraic closure, let , and let be the inseparable degree (The inseparable degree of a finite extension). Then for every ,
and
In particular, when is separable these are the ordinary sum and product over the distinct -embeddings of into ; and when in characteristic , the trace map is identically zero because is a power of .
Facts & Assumptions
Given: A finite extension , an algebraic closure , the set of -embeddings, an element , the separable closure of in , and the inseparable degree .
Norm and trace are defined from the multiplication operator on the finite-dimensional -vector space (The norm and trace of a finite field extension).
The distinct automorphisms of a field are linearly independent after restriction to the multiplicative group, and the same evaluation-matrix argument applies to the distinct -embeddings of a finite separable extension (Dedekind's linear independence theorem for distinct characters).
The separable degree counts the -embeddings into , the inseparable degree is the quotient , and (The separable degree as a count of embeddings into an algebraic closure, The inseparable degree of a finite extension, , and in positive characteristic the inseparable degree is a power of ).
If is the separable closure of in , then and is purely inseparable (For a finite extension, , An algebraic extension is purely inseparable over its separable closure).
For a purely inseparable extension, the inclusion into an algebraic closure is the only embedding over the base field (Pure inseparability and its conjugate, embedding, and separable-degree criteria).
Proof
Suppose first that is separable. Choose an -basis of , list the embeddings as , and form the evaluation matrix . By the same argument used in Artin's fixed-field lower bound, [L1] makes invertible.
For general , let be the separable closure of in . By [L3], the extension is purely inseparable of degree , and the -embeddings of are exactly the extensions of the embeddings of , one extension for each embedding because [L4] gives uniqueness over . Thus may be identified with , and its cardinality is .
Let be the matrix of in the basis . Because for every , one has Hence so determinant and trace of [F1] give
Choose an -basis of and a -basis of , where . Writing the matrix of on the product basis is the block matrix , where is the matrix of multiplication by on . Conjugating each block by the separable evaluation matrix of step 1.1 for turns into a block-diagonal matrix with diagonal blocks as runs through . Therefore
Over , the extension is purely inseparable of degree , so every conjugate of over equals . Accordingly the characteristic polynomial of the -linear operator represented by is , and therefore Applying each in step 3.1 gives
Substituting step 4.1 into step 3.1 yields and This is the stated formula, with the separable case already proved in step 2.1.
If and , then [L2] makes a positive power of , so . The trace formula of step 5.1 is then identically zero.
Remarks
-
The inseparable exponent is load-bearing. In the separable case the norm is the product over the embeddings and the trace is their sum; outside the separable case the product must be raised to , and the trace may vanish identically.
-
The finite-field formulas on the earlier page are examples of this theorem. When over , the embeddings are the Frobenius powers and the product and sum become the familiar Frobenius norm and trace.
Depends on
The norm and trace of a finite field extension
Separable algebraic elements and separable extensions
Dedekind's linear independence theorem for distinct characters
The separable degree as a count of embeddings into an algebraic closure
The inseparable degree of a finite extension
For a finite extension,
An algebraic extension is purely inseparable over its separable closure
Pure inseparability and its conjugate, embedding, and separable-degree criteria
, and in positive characteristic the inseparable degree is a power of
The degree of a finite field extension