# 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.trace R S x: the trace of an element s of an R-algebra S
• Algebra.traceForm R S: bilinear form sending x, y to the trace of x * y
• Algebra.traceMatrix R b: the matrix whose (i j)-th element is the trace of b i * b j.
• 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).

## Main results #

• trace_algebraMap_of_basis, trace_algebraMap: if x : K, then Tr_{L/K} x = [L : K] x
• trace_trace_of_basis, trace_trace: Tr_{L/K} (Tr_{F/L} x) = Tr_{F/K} x
• trace_eq_sum_roots: the trace of x : K(x) is the sum of all conjugate roots of x
• 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
• traceForm_dualBasis_powerBasis_eq: The dual basis of a powerbasis {1, x, x²...} under the trace form is aᵢ / f'(x), with f being the minpoly of x and f / (X - x) = ∑ aᵢxⁱ.

## Implementation notes #

Typically, the trace is defined specifically for finite field extensions. The definition is as general as possible and the assumption that we have fields or that the extension is finite is added to the lemmas as needed.

We only define the trace for left multiplication (Algebra.leftMulMatrix, i.e. LinearMap.mulLeft). For now, the definitions assume S is commutative, so the choice doesn't matter anyway.

## References #

• https://en.wikipedia.org/wiki/Field_trace
noncomputable def Algebra.trace (R : Type u_1) (S : Type u_2) [] [] [Algebra R S] :

The trace of an element s of an R-algebra is the trace of (s * ·), as an R-linear map.

Equations
• = ∘ₗ ().toLinearMap
Instances For
theorem Algebra.trace_apply (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] (x : S) :
() x = () (() x)
theorem Algebra.trace_eq_zero_of_not_exists_basis (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] (h : ¬∃ (s : ), Nonempty (Basis { x : S // x s } R S)) :
= 0
theorem Algebra.trace_eq_matrix_trace {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {ι : Type w} [] [] (b : Basis ι R S) (s : S) :
() s = ().trace
theorem Algebra.trace_algebraMap_of_basis {R : Type u_1} {S : Type u_2} [] [] [Algebra R S] {ι : Type w} [] (b : Basis ι R S) (x : R) :
() (() x) =

If x is in the base field K, then the trace is [L : K] * x.

@[simp]
theorem Algebra.trace_algebraMap {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] (x : K) :
() (() x) =

If x is in the base field K, then the trace is [L : K] * x.

(If L is not finite-dimensional over K, then trace and finrank return 0.)

theorem Algebra.trace_trace_of_basis {R : Type u_1} {S : Type u_2} {T : Type u_3} [] [] [] [Algebra R S] [Algebra R T] [Algebra S T] [] {ι : Type u_6} {κ : Type u_7} [] [] (b : Basis ι R S) (c : Basis κ S T) (x : T) :
() (() x) = () x
theorem Algebra.trace_comp_trace_of_basis {R : Type u_1} {S : Type u_2} {T : Type u_3} [] [] [] [Algebra R S] [Algebra R T] [Algebra S T] [] {ι : Type u_6} {κ : Type u_7} [] [] (b : Basis ι R S) (c : Basis κ S T) :
∘ₗ R () =
@[simp]
theorem Algebra.trace_trace {T : Type u_3} [] {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] [Algebra K T] [Algebra L T] [] [] [] (x : T) :
() (() x) = () x
@[simp]
theorem Algebra.trace_comp_trace {T : Type u_3} [] {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] [Algebra K T] [Algebra L T] [] [] [] :
∘ₗ K () =
@[simp]
theorem Algebra.trace_prod_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} [] [] [] [Algebra R S] [Algebra R T] [] [] [] [] (x : S × T) :
(Algebra.trace R (S × T)) x = () x.1 + () x.2
theorem Algebra.trace_prod {R : Type u_1} {S : Type u_2} {T : Type u_3} [] [] [] [Algebra R S] [Algebra R T] [] [] [] [] :
Algebra.trace R (S × T) = ().coprod ()
noncomputable def Algebra.traceForm (R : Type u_1) (S : Type u_2) [] [] [Algebra R S] :

The traceForm maps x y : S to the trace of x * y. It is a symmetric bilinear form and is nondegenerate if the extension is separable.

Equations
• = ().toLinearMap.compr₂ ()
Instances For
@[simp]
theorem Algebra.traceForm_apply (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] (x : S) (y : S) :
(() x) y = () (x * y)
theorem Algebra.traceForm_isSymm (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] :
().IsSymm
theorem Algebra.traceForm_toMatrix (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] {ι : Type w} [] (b : Basis ι R S) [] (i : ι) (j : ι) :
() i j = () (b i * b j)
theorem Algebra.traceForm_toMatrix_powerBasis (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] (h : ) :
(BilinForm.toMatrix h.basis) () = Matrix.of fun (i j : Fin h.dim) => () (h.gen ^ (i + j))
theorem PowerBasis.trace_gen_eq_nextCoeff_minpoly {S : Type u_2} [] {K : Type u_4} [] [Algebra K S] [] (pb : ) :
() pb.gen = -(minpoly K pb.gen).nextCoeff

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

theorem PowerBasis.trace_gen_eq_sum_roots {S : Type u_2} [] {K : Type u_4} [] {F : Type u_6} [] [Algebra K S] [Algebra K F] [] (pb : ) (hf : Polynomial.Splits () (minpoly K pb.gen)) :
() (() 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.

theorem IntermediateField.AdjoinSimple.trace_gen_eq_zero {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] {x : L} (hx : ¬) :
(Algebra.trace K Kx) = 0
theorem IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] {F : Type u_6} [] [Algebra K F] (x : L) (hf : Polynomial.Splits () (minpoly K x)) :
() ((Algebra.trace K Kx) ) = ((minpoly K x).aroots F).sum
theorem trace_eq_trace_adjoin (K : Type u_4) {L : Type u_5} [] [] [Algebra K L] [] (x : L) :
() x = FiniteDimensional.finrank (Kx) L (Algebra.trace K Kx)
theorem trace_eq_sum_roots {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] {F : Type u_6} [] [Algebra K F] [] {x : L} (hF : Polynomial.Splits () (minpoly K x)) :
() (() x) = FiniteDimensional.finrank (Kx) L ((minpoly K x).aroots F).sum
theorem Algebra.isIntegral_trace {R : Type u_1} [] {L : Type u_5} [] {F : Type u_6} [] [Algebra R L] [Algebra L F] [Algebra R F] [] [] {x : F} (hx : ) :
IsIntegral R (() x)
theorem Algebra.trace_eq_of_algEquiv {A : Type u_7} {B : Type u_8} {C : Type u_9} [] [] [] [Algebra A B] [Algebra A C] (e : B ≃ₐ[A] C) (x : B) :
() (e x) = () x
theorem Algebra.trace_eq_of_ringEquiv {A : Type u_7} {B : Type u_8} {C : Type u_9} [] [] [] [Algebra A C] [Algebra B C] (e : A ≃+* B) (he : ().comp e = ) (x : C) :
e (() x) = () x
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₁) :
(Algebra.trace A₁ B₁) x = e₁.symm ((Algebra.trace A₂ B₂) (e₂ x))
theorem trace_eq_sum_embeddings_gen {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] (E : Type u_7) [] [Algebra K E] (pb : ) (hE : Polynomial.Splits () (minpoly K pb.gen)) (hfx : (minpoly K pb.gen).Separable) :
() (() pb.gen) = Finset.univ.sum fun (σ : L →ₐ[K] E) => σ pb.gen
theorem sum_embeddings_eq_finrank_mul {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] (F : Type u_6) [] [Algebra L F] [Algebra K F] [] (E : Type u_7) [] [Algebra K E] [] [] [] (pb : ) :
(Finset.univ.sum fun (σ : F →ₐ[K] E) => σ (() pb.gen)) = Finset.univ.sum fun (σ : L →ₐ[K] E) => σ pb.gen
theorem trace_eq_sum_embeddings {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] (E : Type u_7) [] [Algebra K E] [] [] [] {x : L} :
() (() x) = Finset.univ.sum fun (σ : L →ₐ[K] E) => σ x
theorem trace_eq_sum_automorphisms {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] (x : L) [] [IsGalois K L] :
() (() x) = Finset.univ.sum fun (σ : L ≃ₐ[K] L) => σ x
noncomputable def Algebra.traceMatrix {κ : Type w} (A : Type u) {B : Type v} [] [] [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
• = Matrix.of fun (i j : κ) => (() (b i)) (b j)
Instances For
@[simp]
theorem Algebra.traceMatrix_apply {κ : Type w} (A : Type u) {B : Type v} [] [] [Algebra A B] (b : κB) (i : κ) (j : κ) :
= (() (b i)) (b j)
theorem Algebra.traceMatrix_reindex {κ : Type w} (A : Type u) {B : Type v} [] [] [Algebra A B] {κ' : Type u_7} (b : Basis κ A B) (f : κ κ') :
Algebra.traceMatrix A (b.reindex f) = () ()
theorem Algebra.traceMatrix_of_matrix_vecMul {κ : Type w} {A : Type u} {B : Type v} [] [] [Algebra A B] [] (b : κB) (P : Matrix κ κ A) :
Algebra.traceMatrix A (Matrix.vecMul b (P.map ())) = P.transpose * * P
theorem Algebra.traceMatrix_of_matrix_mulVec {κ : Type w} {A : Type u} {B : Type v} [] [] [Algebra A B] [] (b : κB) (P : Matrix κ κ A) :
Algebra.traceMatrix A ((P.map ()).mulVec b) = P * * P.transpose
theorem Algebra.traceMatrix_of_basis {κ : Type w} {A : Type u} {B : Type v} [] [] [Algebra A B] [] [] (b : Basis κ A B) :
= ()
theorem Algebra.traceMatrix_of_basis_mulVec {ι : Type w} [] {A : Type u} {B : Type v} [] [] [Algebra A B] (b : Basis ι A B) (z : B) :
().mulVec (b.equivFun z) = fun (i : ι) => () (z * b i)
def Algebra.embeddingsMatrix {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [] [] [Algebra A B] [] [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
• = Matrix.of fun (i : κ) (σ : B →ₐ[A] C) => σ (b i)
Instances For
@[simp]
theorem Algebra.embeddingsMatrix_apply {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [] [] [Algebra A B] [] [Algebra A C] (b : κB) (i : κ) (σ : B →ₐ[A] C) :
= σ (b i)
def Algebra.embeddingsMatrixReindex {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [] [] [Algebra A B] [] [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
Instances For
theorem Algebra.embeddingsMatrixReindex_eq_vandermonde {A : Type u} {B : Type v} (C : Type z) [] [] [Algebra A B] [] [Algebra A C] (pb : ) (e : Fin pb.dim (B →ₐ[A] C)) :
Algebra.embeddingsMatrixReindex A C (pb.basis) e = (Matrix.vandermonde fun (i : Fin pb.dim) => (e i) pb.gen).transpose
theorem Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans (K : Type u_4) {L : Type u_5} [] [] [Algebra K L] {κ : Type w} (E : Type z) [] [Algebra K E] [] [] [] (b : κL) :
().map () = * ().transpose
theorem Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans (K : Type u_4) {L : Type u_5} [] [] [Algebra K L] {κ : Type w} (E : Type z) [] [Algebra K E] [] [] [] (b : κL) [] (e : κ (L →ₐ[K] E)) :
().map () = * ().transpose
theorem det_traceMatrix_ne_zero' {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] (pb : ) [] :
(Algebra.traceMatrix K pb.basis).det 0
theorem det_traceForm_ne_zero {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] {ι : Type w} [] [] [] (b : Basis ι K L) :
( ()).det 0
theorem traceForm_nondegenerate (K : Type u_4) (L : Type u_5) [] [] [Algebra K L] [] [] :
().Nondegenerate
theorem Algebra.trace_ne_zero (K : Type u_4) (L : Type u_5) [] [] [Algebra K L] [] [] :
0
theorem Algebra.trace_surjective (K : Type u_4) (L : Type u_5) [] [] [Algebra K L] [] [] :
theorem traceForm_dualBasis_powerBasis_eq {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] [] [] (pb : ) (i : Fin pb.dim) :
(().dualBasis pb.basis) 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ⁱ.