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 $N_{K/F}$ and trace $\operatorname{Tr}_{K/F}$ of a finite field extension
- Separable algebraic elements and separable extensions
- Dedekind's linear independence theorem for distinct characters
- The separable degree $[K:F]_s$ as a count of embeddings into an algebraic closure
- The inseparable degree $[K:F]_i=[K:F]/[K:F]_s$ of a finite extension
- For a finite extension, $[K:F]_s=[K_s:F]$
- An algebraic extension is purely inseparable over its separable closure
- Pure inseparability and its conjugate, embedding, and separable-degree criteria
- $[K:F]=[K:F]_s[K:F]_i$, and in positive characteristic the inseparable degree is a power of $p$
- The degree $[K:F]=\dim_F K$ of a finite field extension
Used by
- For Fₚ(t)/Fₚ(tᵖ), the trace is identically zero Example
- For ℚ(√d)/ℚ, the embedding formulas match the determinant and trace of multiplication Example
- In F_qⁿ/F_q, norm and trace are the Frobenius product and sum Example
- Over ℚ(ω), the splitting field of x³-2 is a cyclic cubic extension Example
- ℚ(ζ₃,³√2,³√3) is a Kummer extension with quotient (ℤ/3)² Example
- FALSE: for every finite extension, the norm is just the product over the embeddings False statement
- Hilbert's theorem 90 for a finite cyclic extension Theorem
- Norm is multiplicative, trace is F-linear, and both are transitive in towers Theorem
- The trace form of a finite extension is nondegenerate exactly when the extension is separable Theorem
Dependency tree · two levels
36 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, Corollary 5.45 and Remark 5.47 (standard reference, not scraped)
- B. Conrad, Norm and trace, Theorems 2.3 and 3.2 (standard reference, not scraped)