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).

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
• 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ⁱ.

References

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

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) (Algebra.traceForm R S) = Matrix.of fun (i j : Fin h.dim) => (Algebra.trace R S) (h.gen ^ (↑i + ↑j))

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.

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.

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⟯) (IntermediateField.AdjoinSimple.gen K x) = 0

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⟯) (IntermediateField.AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).sum

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)

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

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 ((Algebra.trace L F) x)

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) : (Algebra.trace A C) (e x) = (Algebra.trace A B) x

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 ((Algebra.trace A C) x) = (Algebra.trace B C) 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} [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

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

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

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) = ∑ σ : L ≃ₐ[K] L, σ x

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)

@[simp]

theorem Algebra.traceMatrix_apply {κ : Type w} (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (b : κ → B) (i : κ) (j : κ) : Algebra.traceMatrix A b i j = ((Algebra.traceForm A B) (b i)) (b j)

theorem Algebra.traceMatrix_reindex {κ : Type w} (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {κ' : Type u_7} (b : Basis κ A B) (f : κ ≃ κ') : Algebra.traceMatrix A ⇑(b.reindex f) = (Matrix.reindex f f) (Algebra.traceMatrix A ⇑b)

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) : Algebra.traceMatrix A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.transpose * Algebra.traceMatrix A b * P

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) : Algebra.traceMatrix A ((P.map ⇑(algebraMap A B)).mulVec b) = P * Algebra.traceMatrix A b * P.transpose

theorem Algebra.traceMatrix_of_basis {κ : Type w} {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype κ] [DecidableEq κ] (b : Basis κ A B) : Algebra.traceMatrix A ⇑b = (BilinForm.toMatrix b) (Algebra.traceForm A B)

theorem Algebra.traceMatrix_of_basis_mulVec {ι : Type w} [Fintype ι] {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (b : Basis ι A B) (z : B) : (Algebra.traceMatrix A ⇑b).mulVec (b.equivFun z) = fun (i : ι) => (Algebra.trace A B) (z * b i)

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)

@[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) : Algebra.embeddingsMatrix A C b i σ = σ (b i)

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)

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)) : 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} [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) : (Algebra.traceMatrix K b).map ⇑(algebraMap K E) = Algebra.embeddingsMatrix K E b * (Algebra.embeddingsMatrix K E b).transpose

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)) : (Algebra.traceMatrix K b).map ⇑(algebraMap K E) = Algebra.embeddingsMatrixReindex K E b e * (Algebra.embeddingsMatrixReindex K E b e).transpose

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

theorem det_traceForm_ne_zero {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] {ι : Type w} [Fintype ι] [Algebra.IsSeparable K L] [DecidableEq ι] (b : Basis ι K L) : ((BilinForm.toMatrix b) (Algebra.traceForm K L)).det ≠ 0

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

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] : Algebra.trace K L ≠ 0

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 ⇑(Algebra.trace K L)

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) : ((Algebra.traceForm K L).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ⁱ.

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 ((Algebra.trace R S) x)

The trace of a nilpotent element is nilpotent.