# Trace for (finite) ring extensions. #

Suppose we have an `R`-algebra `S` with a finite basis. For each `s : S`, the trace of the linear map given by multiplying by `s` gives information about the roots of the minimal polynomial of `s` over `R`.

## Main definitions #

- `Algebra.embeddingsMatrix A C b : Matrix κ (B →ₐ[A] C) C` is the matrix whose `(i, σ)` coefficient is `σ (b i)`.
- `Algebra.embeddingsMatrixReindex A C b e : Matrix κ κ C` is the matrix whose `(i, j)` coefficient is `σⱼ (b i)`, where `σⱼ : B →ₐ[A] C` is the embedding corresponding to `j : κ` given by a bijection `e : κ ≃ (B →ₐ[A] C)`.
- `Module.Basis.traceDual`: The dual basis of a basis under the trace form in a finite separable extension.

## Main results #

- `trace_eq_sum_embeddings`: the trace of `x : K(x)` is the sum of all embeddings of `x` into an algebraically closed field
- `traceForm_nondegenerate`: the trace form over a separable extension is a nondegenerate bilinear form
- `Module.Basis.traceDual_powerBasis_eq`: The dual basis of a power basis `{1, x, x²...}` under the trace form is `aᵢ / f'(x)`, with `f` being the minpoly of `x` and `f / (X - x) = ∑ aᵢxⁱ`.

## References #

- https://en.wikipedia.org/wiki/Field_trace

source
theorem Algebra.traceForm_toMatrix_powerBasis {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (h : PowerBasis R S) :
(BilinForm.toMatrix h.basis) (traceForm R S) = Matrix.of fun (i j : Fin h.dim) => (trace R S) (h.gen ^ (↑i + ↑j))
source
theorem PowerBasis.trace_gen_eq_nextCoeff_minpoly {S : Type u_2} [CommRing S] {K : Type u_4} [Field K] [Algebra K S] [Nontrivial S] (pb : PowerBasis K S) :
(Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Given `pb : PowerBasis K S`, the trace of `pb.gen` is `-(minpoly K pb.gen).nextCoeff`.

source
theorem PowerBasis.trace_gen_eq_sum_roots {S : Type u_2} [CommRing S] {K : Type u_4} [Field K] {F : Type u_6} [Field F] [Algebra K S] [Algebra K F] [Nontrivial S] (pb : PowerBasis K S) (hf : Polynomial.Splits (algebraMap K F) (minpoly K pb.gen)) :
(algebraMap K F) ((Algebra.trace K S) pb.gen) = ((minpoly K pb.gen).aroots F).sum

Given `pb : PowerBasis K S`, then the trace of `pb.gen` is `((minpoly K pb.gen).aroots F).sum`.

source
theorem IntermediateField.AdjoinSimple.trace_gen_eq_zero {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {x : L} (hx : ¬IsIntegral K x) :
(Algebra.trace K ↥K⟮x⟯) (gen K x) = 0
source
theorem IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {F : Type u_6} [Field F] [Algebra K F] (x : L) (hf : Polynomial.Splits (algebraMap K F) (minpoly K x)) :
(algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum
source
theorem trace_eq_trace_adjoin (K : Type u_4) {L : Type u_5} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (x : L) :
(Algebra.trace K L) x = Module.finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x)
source
theorem trace_adjoinSimpleGen {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) :
(Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x) = -(minpoly K x).nextCoeff

Trace of the generator of a simple adjoin equals negative of the next coefficient of its minimal polynomial coefficient.

source
theorem trace_eq_finrank_mul_minpoly_nextCoeff (K : Type u_4) {L : Type u_5} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (x : L) :
(Algebra.trace K L) x = ↑(Module.finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff
source
theorem trace_eq_sum_roots {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {F : Type u_6} [Field F] [Algebra K F] [FiniteDimensional K L] {x : L} (hF : Polynomial.Splits (algebraMap K F) (minpoly K x)) :
(algebraMap K F) ((Algebra.trace K L) x) = Module.finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum
source
theorem Algebra.isIntegral_trace {R : Type u_1} [CommRing R] {L : Type u_5} [Field L] {F : Type u_6} [Field F] [Algebra R L] [Algebra L F] [Algebra R F] [IsScalarTower R L F] [FiniteDimensional L F] {x : F} (hx : IsIntegral R x) :
IsIntegral R ((trace L F) x)
source
theorem Algebra.trace_eq_of_algEquiv {A : Type u_7} {B : Type u_8} {C : Type u_9} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] (e : B ≃ₐ[A] C) (x : B) :
(trace A C) (e x) = (trace A B) x
source
theorem Algebra.trace_eq_of_ringEquiv {A : Type u_7} {B : Type u_8} {C : Type u_9} [CommRing A] [CommRing B] [CommRing C] [Algebra A C] [Algebra B C] (e : A ≃+* B) (he : (algebraMap B C).comp ↑e = algebraMap A C) (x : C) :
e ((trace A C) x) = (trace B C) x
source
theorem Algebra.trace_eq_of_equiv_equiv {A₁ : Type u_7} {B₁ : Type u_8} {A₂ : Type u_9} {B₂ : Type u_10} [CommRing A₁] [CommRing B₁] [CommRing A₂] [CommRing B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂) (he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)) (x : B₁) :
(trace A₁ B₁) x = e₁.symm ((trace A₂ B₂) (e₂ x))
source
theorem trace_eq_sum_embeddings_gen {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (E : Type u_7) [Field E] [Algebra K E] (pb : PowerBasis K L) (hE : Polynomial.Splits (algebraMap K E) (minpoly K pb.gen)) (hfx : IsSeparable K pb.gen) :
(algebraMap K E) ((Algebra.trace K L) pb.gen) = ∑ σ : L →ₐ[K] E, σ pb.gen
source
theorem sum_embeddings_eq_finrank_mul {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (F : Type u_6) [Field F] [Algebra L F] [Algebra K F] [IsScalarTower K L F] (E : Type u_7) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K F] [Algebra.IsSeparable K F] (pb : PowerBasis K L) :
∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = Module.finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen
source
theorem trace_eq_sum_embeddings {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (E : Type u_7) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K L] [Algebra.IsSeparable K L] {x : L} :
(algebraMap K E) ((Algebra.trace K L) x) = ∑ σ : L →ₐ[K] E, σ x
source
theorem trace_eq_sum_automorphisms {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (x : L) [FiniteDimensional K L] [IsGalois K L] :
(algebraMap K L) ((Algebra.trace K L) x) = ∑ σ : Gal(L/K), σ x
source
theorem Algebra.trace_eq_zero_of_not_isSeparable {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (H : ¬Algebra.IsSeparable K L) :
trace K L = 0
source
noncomputable def Algebra.traceMatrix {κ : Type w} (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (b : κ → B) :
Matrix κ κ A

Given an `A`-algebra `B` and `b`, a `κ`-indexed family of elements of `B`, we define `traceMatrix A b` as the matrix whose `(i j)`-th element is the trace of `b i * b j`.

Equations

- Algebra.traceMatrix A b = Matrix.of fun (i j : κ) => ((Algebra.traceForm A B) (b i)) (b j)

Instances For

source
@[simp]
theorem Algebra.traceMatrix_apply {κ : Type w} (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (b : κ → B) (i j : κ) :
traceMatrix A b i j = ((traceForm A B) (b i)) (b j)
source
theorem Algebra.traceMatrix_reindex {κ : Type w} (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {κ' : Type u_7} (b : Module.Basis κ A B) (f : κ ≃ κ') :
traceMatrix A ⇑(b.reindex f) = (Matrix.reindex f f) (traceMatrix A ⇑b)
source
theorem Algebra.traceMatrix_of_matrix_vecMul {κ : Type w} {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype κ] (b : κ → B) (P : Matrix κ κ A) :
traceMatrix A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.transpose * traceMatrix A b * P
source
theorem Algebra.traceMatrix_of_matrix_mulVec {κ : Type w} {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype κ] (b : κ → B) (P : Matrix κ κ A) :
traceMatrix A ((P.map ⇑(algebraMap A B)).mulVec b) = P * traceMatrix A b * P.transpose
source
theorem Algebra.traceMatrix_of_basis {κ : Type w} {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype κ] [DecidableEq κ] (b : Module.Basis κ A B) :
traceMatrix A ⇑b = (BilinForm.toMatrix b) (traceForm A B)
source
theorem Algebra.traceMatrix_of_basis_mulVec {ι : Type w} {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : Module.Basis ι A B) (z : B) :
(traceMatrix A ⇑b).mulVec (b.equivFun z) = fun (i : ι) => (trace A B) (z * b i)
source
def Algebra.embeddingsMatrix {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [CommRing A] [CommRing B] [Algebra A B] [CommRing C] [Algebra A C] (b : κ → B) :
Matrix κ (B →ₐ[A] C) C

`embeddingsMatrix A C b : Matrix κ (B →ₐ[A] C) C` is the matrix whose `(i, σ)` coefficient is `σ (b i)`. It is mostly useful for fields when `Fintype.card κ = finrank A B` and `C` is algebraically closed.

Equations

- Algebra.embeddingsMatrix A C b = Matrix.of fun (i : κ) (σ : B →ₐ[A] C) => σ (b i)

Instances For

source
@[simp]
theorem Algebra.embeddingsMatrix_apply {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [CommRing A] [CommRing B] [Algebra A B] [CommRing C] [Algebra A C] (b : κ → B) (i : κ) (σ : B →ₐ[A] C) :
embeddingsMatrix A C b i σ = σ (b i)
source
def Algebra.embeddingsMatrixReindex {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [CommRing A] [CommRing B] [Algebra A B] [CommRing C] [Algebra A C] (b : κ → B) (e : κ ≃ (B →ₐ[A] C)) :
Matrix κ κ C

`embeddingsMatrixReindex A C b e : Matrix κ κ C` is the matrix whose `(i, j)` coefficient is `σⱼ (b i)`, where `σⱼ : B →ₐ[A] C` is the embedding corresponding to `j : κ` given by a bijection `e : κ ≃ (B →ₐ[A] C)`. It is mostly useful for fields and `C` is algebraically closed. In this case, in presence of `h : Fintype.card κ = finrank A B`, one can take `e := equivOfCardEq ((AlgHom.card A B C).trans h.symm)`.

Equations

- Algebra.embeddingsMatrixReindex A C b e = (Matrix.reindex (Equiv.refl κ) e.symm) (Algebra.embeddingsMatrix A C b)

Instances For

source
theorem Algebra.embeddingsMatrixReindex_eq_vandermonde {A : Type u} {B : Type v} (C : Type z) [CommRing A] [CommRing B] [Algebra A B] [CommRing C] [Algebra A C] (pb : PowerBasis A B) (e : Fin pb.dim ≃ (B →ₐ[A] C)) :
embeddingsMatrixReindex A C (⇑pb.basis) e = (Matrix.vandermonde fun (i : Fin pb.dim) => (e i) pb.gen).transpose
source
theorem Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans (K : Type u_4) {L : Type u_5} [Field K] [Field L] [Algebra K L] {κ : Type w} (E : Type z) [Field E] [Algebra K E] [Module.Finite K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (b : κ → L) :
(traceMatrix K b).map ⇑(algebraMap K E) = embeddingsMatrix K E b * (embeddingsMatrix K E b).transpose
source
theorem Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans (K : Type u_4) {L : Type u_5} [Field K] [Field L] [Algebra K L] {κ : Type w} (E : Type z) [Field E] [Algebra K E] [Module.Finite K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (b : κ → L) [Fintype κ] (e : κ ≃ (L →ₐ[K] E)) :
(traceMatrix K b).map ⇑(algebraMap K E) = embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e).transpose
source
theorem det_traceMatrix_ne_zero' {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] (pb : PowerBasis K L) [Algebra.IsSeparable K L] :
(Algebra.traceMatrix K ⇑pb.basis).det ≠ 0
source
theorem det_traceForm_ne_zero {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [Algebra.IsSeparable K L] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K L) :
((BilinForm.toMatrix b) (Algebra.traceForm K L)).det ≠ 0
source
theorem traceForm_nondegenerate (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] :
(Algebra.traceForm K L).Nondegenerate

Let $L/K$ be a finite extension of fields. If $L/K$ is separable, then `traceForm` is nondegenerate.

source
theorem traceForm_nondegenerate_tfae (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] :
[Algebra.IsSeparable K L, Algebra.trace K L ≠ 0, (Algebra.traceForm K L).Nondegenerate].TFAE

Stacks Tag 0BIL

source
theorem Algebra.trace_ne_zero (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] :
trace K L ≠ 0
source
theorem Algebra.trace_surjective (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] :
Function.Surjective ⇑(trace K L)
source
theorem Algebra.isNilpotent_trace_of_isNilpotent {R : Type u_7} {S : Type u_8} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsNilpotent x) :
IsNilpotent ((trace R S) x)

The trace of a nilpotent element is nilpotent.

source
@[deprecated Algebra.isNilpotent_trace_of_isNilpotent (since := "2025-10-21")]
theorem Algebra.trace_isNilpotent_of_isNilpotent {R : Type u_7} {S : Type u_8} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsNilpotent x) :
IsNilpotent ((trace R S) x)

Alias of `Algebra.isNilpotent_trace_of_isNilpotent`.

The trace of a nilpotent element is nilpotent.

source
noncomputable def Module.Basis.traceDual {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] (b : Basis ι K L) :
Basis ι K L

The dual basis of a basis under the trace form in a finite separable extension.

Equations

- b.traceDual = (Algebra.traceForm K L).dualBasis ⋯ b

Instances For

source
theorem Module.Basis.traceDual_def {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] (b : Basis ι K L) :
b.traceDual = (Algebra.traceForm K L).dualBasis ⋯ b
source
@[simp]
theorem Module.Basis.traceDual_repr_apply {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] (b : Basis ι K L) (x : L) (i : ι) :
(b.traceDual.repr x) i = ((Algebra.traceForm K L) x) (b i)
source
@[simp]
theorem Module.Basis.trace_traceDual_mul {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] (b : Basis ι K L) (i j : ι) :
(Algebra.trace K L) (b.traceDual i * b j) = if j = i then 1 else 0
source
@[simp]
theorem Module.Basis.trace_mul_traceDual {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] (b : Basis ι K L) (i j : ι) :
(Algebra.trace K L) (b i * b.traceDual j) = if i = j then 1 else 0
source
@[simp]
theorem Module.Basis.traceDual_traceDual {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] (b : Basis ι K L) :
b.traceDual.traceDual = b
source
theorem Module.Basis.traceDual_involutive (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] :
Function.Involutive traceDual
source
theorem Module.Basis.traceDual_injective (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] :
Function.Injective traceDual
source
@[simp]
theorem Module.Basis.traceDual_inj {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] {b b' : Basis ι K L} :
b.traceDual = b'.traceDual ↔ b = b'
source
@[simp]
theorem Module.Basis.traceDual_eq_iff {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [FiniteDimensional K L] [Algebra.IsSeparable K L] [Finite ι] [DecidableEq ι] {b : Basis ι K L} {v : ι → L} :
⇑b.traceDual = v ↔ ∀ (i j : ι), ((Algebra.traceForm K L) (v i)) (b j) = if j = i then 1 else 0

A family of vectors `v` is the dual for the trace of the basis `b` if and only if `∀ i j, Tr(v i * b j) = δ_ij`.

source
theorem Module.Basis.traceDual_powerBasis_eq {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (pb : PowerBasis K L) (i : Fin pb.dim) :
pb.basis.traceDual i = (minpolyDiv K pb.gen).coeff ↑i / (Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen))

The dual basis of a powerbasis `{1, x, x²...}` under the trace form is `aᵢ / f'(x)`, with `f` being the minimal polynomial of `x` and `f / (X - x) = ∑ aᵢxⁱ`.

source
@[deprecated Module.Basis.traceDual_powerBasis_eq (since := "2025-06-25")]
theorem traceForm_dualBasis_powerBasis_eq {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (pb : PowerBasis K L) (i : Fin pb.dim) :
pb.basis.traceDual i = (minpolyDiv K pb.gen).coeff ↑i / (Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen))

Alias of `Module.Basis.traceDual_powerBasis_eq`.

The dual basis of a powerbasis `{1, x, x²...}` under the trace form is `aᵢ / f'(x)`, with `f` being the minimal polynomial of `x` and `f / (X - x) = ∑ aᵢxⁱ`.