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) Cis the matrix whose(i, σ)coefficient isσ (b i).Algebra.embeddingsMatrixReindex A C b e : Matrix κ κ Cis the matrix whose(i, j)coefficient isσⱼ (b i), whereσⱼ : B →ₐ[A] Cis the embedding corresponding toj : κgiven by a bijectione : κ ≃ (B →ₐ[A] C).
Main results #
trace_eq_sum_embeddings: the trace ofx : K(x)is the sum of all embeddings ofxinto an algebraically closed fieldtraceForm_nondegenerate: the trace form over a separable extension is a nondegenerate bilinear formtraceForm_dualBasis_powerBasis_eq: The dual basis of a power basis{1, x, x²...}under the trace form isaᵢ / f'(x), withfbeing the minpoly ofxandf / (X - x) = ∑ aᵢxⁱ.
References #
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)
:
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))
:
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))
:
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_adjoinSimpleGen
{K : Type u_4}
{L : Type u_5}
[Field K]
[Field L]
[Algebra K L]
{x : L}
(hx : IsIntegral K x)
:
Trace of the generator of a simple adjoin equals negative of the next coefficient of its minimal polynomial coefficient.
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)
:
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))
:
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)
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₁)
:
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)
:
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)
:
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}
:
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]
:
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
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 : κ ≃ κ')
:
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)
:
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)
:
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
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
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
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
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
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]
:
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 : Module.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]
:
Let $L/K$ be a finite extension of fields. If $L/K$ is separable,
then traceForm is nondegenerate.
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
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
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)
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 power basis {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 ((trace R S) x)
The trace of a nilpotent element is nilpotent.