Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26
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 K/F be a finite field extension, let Ω/F be an algebraic closure, let Σ=HomF(K,Ω), and let [K:F]i be the inseparable degree (The inseparable degree [K:F]i=[K:F]/[K:F]s of a finite extension). Then for every aK,

TrK/F(a)=[K:F]iσΣσ(a),

and

NK/F(a)=(σΣσ(a))[K:F]i.

In particular, when K/F is separable these are the ordinary sum and product over the distinct F-embeddings of K into Ω; and when [K:F]i>1 in characteristic p>0, the trace map is identically zero because [K:F]i is a power of p.

Facts & Assumptions

Given: A finite extension K/F, an algebraic closure Ω/F, the set Σ=HomF(K,Ω) of F-embeddings, an element aK, the separable closure Ks of F in K, and the inseparable degree [K:F]i.

[F1]

Norm and trace are defined from the multiplication operator ma ⁣:xax on the finite-dimensional F-vector space K (The norm NK/F and trace TrK/F of a finite field extension).

[L1]

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 F-embeddings of a finite separable extension (Dedekind's linear independence theorem for distinct characters).

[L3]

If Ks is the separable closure of F in K, then [K:F]s=[Ks:F] and K/Ks is purely inseparable (For a finite extension, [K:F]s=[Ks:F], An algebraic extension is purely inseparable over its separable closure).

[L4]

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

technique · direct
1.1

Suppose first that K/F is separable. Choose an F-basis u1,,un of K, list the embeddings as σ1,,σn, and form the evaluation matrix A=(σi(uj))i,j. By the same argument used in Artin's fixed-field lower bound, [L1] makes A invertible.

L1L2choose
1.2

For general K/F, let Ks be the separable closure of F in K. By [L3], the extension K/Ks is purely inseparable of degree [K:F]i, and the F-embeddings of K are exactly the extensions of the embeddings of Ks, one extension for each embedding because [L4] gives uniqueness over Ks. Thus Σ may be identified with HomF(Ks,Ω), and its cardinality is [K:F]s.

L2L3L4
2.1

Let M be the matrix of ma in the basis u1,,un. Because σi(auj)=σi(a)σi(uj) for every i,j, one has AM=diag(σ1(a),,σn(a))A. Hence M=A1diag(σ1(a),,σn(a))A, so determinant and trace of [F1] give NK/F(a)=iσi(a),TrK/F(a)=iσi(a).

F1step 1.1algebra
3.1

Choose an F-basis v1,,vs of Ks and a Ks-basis b1,,bi of K, where i=[K:F]i. Writing abr=q=1icqrbq(cqrKs), the matrix of ma on the product basis (bqvj) is the block matrix C=(M(cqr))q,r, where M(cqr) is the matrix of multiplication by cqr on Ks/F. Conjugating each block by the separable evaluation matrix of step 1.1 for Ks/F turns C into a block-diagonal matrix with diagonal blocks σ(C) as σ runs through Σ. Therefore NK/F(a)=σΣdet(σ(C)),TrK/F(a)=σΣtr(σ(C)).

F1step 2.1step 1.2algebra
4.1

Over Ks, the extension K/Ks is purely inseparable of degree i, so every conjugate of a over Ks equals a. Accordingly the characteristic polynomial of the Ks-linear operator represented by C is (Xa)i, and therefore det(C)=ai,tr(C)=ia. Applying each σΣ in step 3.1 gives det(σ(C))=σ(a)i,tr(σ(C))=iσ(a).

step 3.1L3L4algebra
5.1

Substituting step 4.1 into step 3.1 yields NK/F(a)=σΣσ(a)i=(σΣσ(a))i, and TrK/F(a)=σΣiσ(a)=iσΣσ(a). This is the stated formula, with the separable case already proved in step 2.1.

step 3.1step 4.1algebra
6.1

If charF=p>0 and i>1, then [L2] makes i a positive power of p, so i1F=0. The trace formula of step 5.1 is then identically zero.

step 5.1L2algebra

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 [K:F]i, and the trace may vanish identically.

  • The finite-field formulas on the earlier page are examples of this theorem. When K=Fqn over Fq, the embeddings are the Frobenius powers and the product and sum become the familiar Frobenius norm and trace.

Depends on

Used by

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