Documentation

Mathlib.RingTheory.Trace.Basic

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 #

Main results #

References #

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) :
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 Kx) (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) :
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 (↥Kx) 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) :
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
Instances For
    @[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) :
    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
    Instances For
      @[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
      Instances For
        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) :
        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)) :
        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) :
        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] :
        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ⁱ.