Trace for (finite) ring extensions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 elementsof anR-algebraSalgebra.trace_form R S: bilinear form sendingx,yto the trace ofx * yalgebra.trace_matrix R b: the matrix whose(i j)-th element is the trace ofb i * b j.algebra.embeddings_matrix A C b : matrix κ (B →ₐ[A] C) Cis the matrix whose(i, σ)coefficient isσ (b i).algebra.embeddings_matrix_reindex 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_algebra_map_of_basis,trace_algebra_map: ifx : K, thenTr_{L/K} x = [L : K] xtrace_trace_of_basis,trace_trace:Tr_{L/K} (Tr_{F/L} x) = Tr_{F/K} xtrace_eq_sum_roots: the trace ofx : K(x)is the sum of all conjugate roots ofxtrace_eq_sum_embeddings: the trace ofx : K(x)is the sum of all embeddings ofxinto an algebraically closed fieldtrace_form_nondegenerate: the trace form over a separable extension is a nondegenerate bilinear form
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.left_mul_matrix,
i.e. linear_map.mul_left).
For now, the definitions assume S is commutative, so the choice doesn't matter anyway.
References #
noncomputable
def
algebra.trace
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
The trace of an element s of an R-algebra is the trace of (*) s,
as an R-linear map.
Equations
- algebra.trace R S = (linear_map.trace R S).comp (algebra.lmul R S).to_linear_map
theorem
algebra.trace_apply
(R : Type u_1)
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
(x : S) :
⇑(algebra.trace R S) x = ⇑(linear_map.trace R S) (⇑(algebra.lmul R S) x)
theorem
algebra.trace_eq_matrix_trace
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{ι : Type w}
[fintype ι]
[decidable_eq ι]
(b : basis ι R S)
(s : S) :
⇑(algebra.trace R S) s = (⇑(algebra.left_mul_matrix b) s).trace
theorem
algebra.trace_algebra_map_of_basis
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{ι : Type w}
[fintype ι]
(b : basis ι R S)
(x : R) :
⇑(algebra.trace R S) (⇑(algebra_map R S) x) = fintype.card ι • x
If x is in the base field K, then the trace is [L : K] * x.
@[simp]
theorem
algebra.trace_algebra_map
{K : Type u_4}
{L : Type u_5}
[field K]
[field L]
[algebra K L]
(x : K) :
⇑(algebra.trace K L) (⇑(algebra_map K L) x) = finite_dimensional.finrank K L • 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}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra R T]
[algebra S T]
[is_scalar_tower R S T]
{ι : Type u_4}
{κ : Type u_5}
[finite ι]
[finite κ]
(b : basis ι R S)
(c : basis κ S T)
(x : T) :
⇑(algebra.trace R S) (⇑(algebra.trace S T) x) = ⇑(algebra.trace R T) x
theorem
algebra.trace_comp_trace_of_basis
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra R T]
[algebra S T]
[is_scalar_tower R S T]
{ι : Type u_4}
{κ : Type u_5}
[finite ι]
[fintype κ]
(b : basis ι R S)
(c : basis κ S T) :
(algebra.trace R S).comp (linear_map.restrict_scalars R (algebra.trace S T)) = algebra.trace R T
@[simp]
theorem
algebra.trace_trace
{T : Type u_3}
[comm_ring T]
{K : Type u_4}
{L : Type u_5}
[field K]
[field L]
[algebra K L]
[algebra K T]
[algebra L T]
[is_scalar_tower K L T]
[finite_dimensional K L]
[finite_dimensional L T]
(x : T) :
⇑(algebra.trace K L) (⇑(algebra.trace L T) x) = ⇑(algebra.trace K T) x
@[simp]
theorem
algebra.trace_comp_trace
{T : Type u_3}
[comm_ring T]
{K : Type u_4}
{L : Type u_5}
[field K]
[field L]
[algebra K L]
[algebra K T]
[algebra L T]
[is_scalar_tower K L T]
[finite_dimensional K L]
[finite_dimensional L T] :
(algebra.trace K L).comp (linear_map.restrict_scalars K (algebra.trace L T)) = algebra.trace K T
@[simp]
theorem
algebra.trace_prod_apply
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra R T]
[module.free R S]
[module.free R T]
[module.finite R S]
[module.finite R T]
(x : S × T) :
⇑(algebra.trace R (S × T)) x = ⇑(algebra.trace R S) x.fst + ⇑(algebra.trace R T) x.snd
theorem
algebra.trace_prod
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra R T]
[module.free R S]
[module.free R T]
[module.finite R S]
[module.finite R T] :
algebra.trace R (S × T) = (algebra.trace R S).coprod (algebra.trace R T)
noncomputable
def
algebra.trace_form
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
bilin_form R S
The trace_form 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
- algebra.trace_form R S = ⇑linear_map.to_bilin ((algebra.lmul R S).to_linear_map.compr₂ (algebra.trace R S))
@[simp]
theorem
algebra.trace_form_apply
(R : Type u_1)
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
(x y : S) :
⇑(algebra.trace_form R S) x y = ⇑(algebra.trace R S) (x * y)
theorem
algebra.trace_form_is_symm
(R : Type u_1)
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S] :
(algebra.trace_form R S).is_symm
theorem
algebra.trace_form_to_matrix
(R : Type u_1)
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{ι : Type w}
[fintype ι]
(b : basis ι R S)
[decidable_eq ι]
(i j : ι) :
⇑(bilin_form.to_matrix b) (algebra.trace_form R S) i j = ⇑(algebra.trace R S) (⇑b i * ⇑b j)
theorem
algebra.trace_form_to_matrix_power_basis
(R : Type u_1)
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
(h : power_basis R S) :
theorem
power_basis.trace_gen_eq_next_coeff_minpoly
{S : Type u_2}
[comm_ring S]
{K : Type u_4}
[field K]
[algebra K S]
[nontrivial S]
(pb : power_basis K S) :
⇑(algebra.trace K S) pb.gen = -(minpoly K pb.gen).next_coeff
Given pb : power_basis K S, the trace of pb.gen is -(minpoly K pb.gen).next_coeff.
theorem
power_basis.trace_gen_eq_sum_roots
{S : Type u_2}
[comm_ring S]
{K : Type u_4}
[field K]
{F : Type u_6}
[field F]
[algebra K S]
[algebra K F]
[nontrivial S]
(pb : power_basis K S)
(hf : polynomial.splits (algebra_map K F) (minpoly K pb.gen)) :
⇑(algebra_map K F) (⇑(algebra.trace K S) pb.gen) = (polynomial.map (algebra_map K F) (minpoly K pb.gen)).roots.sum
Given pb : power_basis K S, then the trace of pb.gen is
((minpoly K pb.gen).map (algebra_map K F)).roots.sum.
theorem
intermediate_field.adjoin_simple.trace_gen_eq_zero
{K : Type u_4}
{L : Type u_5}
[field K]
[field L]
[algebra K L]
{x : L}
(hx : ¬is_integral K x) :
⇑(algebra.trace K ↥K⟮x⟯) (intermediate_field.adjoin_simple.gen K x) = 0
theorem
intermediate_field.adjoin_simple.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 (algebra_map K F) (minpoly K x)) :
⇑(algebra_map K F) (⇑(algebra.trace K ↥K⟮x⟯) (intermediate_field.adjoin_simple.gen K x)) = (polynomial.map (algebra_map K F) (minpoly K x)).roots.sum
theorem
trace_eq_trace_adjoin
(K : Type u_4)
{L : Type u_5}
[field K]
[field L]
[algebra K L]
[finite_dimensional K L]
(x : L) :
⇑(algebra.trace K L) x = finite_dimensional.finrank ↥K⟮x⟯ L • ⇑(algebra.trace K ↥K⟮x⟯) (intermediate_field.adjoin_simple.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]
[finite_dimensional K L]
{x : L}
(hF : polynomial.splits (algebra_map K F) (minpoly K x)) :
⇑(algebra_map K F) (⇑(algebra.trace K L) x) = finite_dimensional.finrank ↥K⟮x⟯ L • (polynomial.map (algebra_map K F) (minpoly K x)).roots.sum
theorem
algebra.is_integral_trace
{R : Type u_1}
[comm_ring R]
{L : Type u_5}
[field L]
{F : Type u_6}
[field F]
[algebra R L]
[algebra L F]
[algebra R F]
[is_scalar_tower R L F]
[finite_dimensional L F]
{x : F}
(hx : is_integral R x) :
is_integral R (⇑(algebra.trace L F) 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 : power_basis K L)
(hE : polynomial.splits (algebra_map K E) (minpoly K pb.gen))
(hfx : (minpoly K pb.gen).separable) :
⇑(algebra_map K E) (⇑(algebra.trace K L) pb.gen) = finset.univ.sum (λ (σ : 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]
[is_scalar_tower K L F]
(E : Type u_7)
[field E]
[algebra K E]
[is_alg_closed E]
[finite_dimensional K F]
[is_separable K F]
(pb : power_basis K L) :
finset.univ.sum (λ (σ : F →ₐ[K] E), ⇑σ (⇑(algebra_map L F) pb.gen)) = finite_dimensional.finrank L F • finset.univ.sum (λ (σ : 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]
[is_alg_closed E]
[finite_dimensional K L]
[is_separable K L]
{x : L} :
⇑(algebra_map K E) (⇑(algebra.trace K L) x) = finset.univ.sum (λ (σ : 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)
[finite_dimensional K L]
[is_galois K L] :
⇑(algebra_map K L) (⇑(algebra.trace K L) x) = finset.univ.sum (λ (σ : L ≃ₐ[K] L), ⇑σ x)
noncomputable
def
algebra.trace_matrix
{κ : Type w}
(A : Type u)
{B : Type v}
[comm_ring A]
[comm_ring B]
[algebra A B]
(b : κ → B) :
matrix κ κ A
Given an A-algebra B and b, an κ-indexed family of elements of B, we define
trace_matrix A b as the matrix whose (i j)-th element is the trace of b i * b j.
Equations
- algebra.trace_matrix A b = ⇑matrix.of (λ (i j : κ), ⇑(algebra.trace_form A B) (b i) (b j))
@[simp]
theorem
algebra.trace_matrix_apply
{κ : Type w}
(A : Type u)
{B : Type v}
[comm_ring A]
[comm_ring B]
[algebra A B]
(b : κ → B)
(i j : κ) :
algebra.trace_matrix A b i j = ⇑(algebra.trace_form A B) (b i) (b j)
theorem
algebra.trace_matrix_reindex
{κ : Type w}
(A : Type u)
{B : Type v}
[comm_ring A]
[comm_ring B]
[algebra A B]
{κ' : Type u_1}
(b : basis κ A B)
(f : κ ≃ κ') :
algebra.trace_matrix A ⇑(b.reindex f) = ⇑(matrix.reindex f f) (algebra.trace_matrix A ⇑b)
theorem
algebra.trace_matrix_of_matrix_vec_mul
{κ : Type w}
{A : Type u}
{B : Type v}
[comm_ring A]
[comm_ring B]
[algebra A B]
[fintype κ]
(b : κ → B)
(P : matrix κ κ A) :
algebra.trace_matrix A (matrix.vec_mul b (P.map ⇑(algebra_map A B))) = (P.transpose.mul (algebra.trace_matrix A b)).mul P
theorem
algebra.trace_matrix_of_basis
{κ : Type w}
{A : Type u}
{B : Type v}
[comm_ring A]
[comm_ring B]
[algebra A B]
[fintype κ]
[decidable_eq κ]
(b : basis κ A B) :
algebra.trace_matrix A ⇑b = ⇑(bilin_form.to_matrix b) (algebra.trace_form A B)
def
algebra.embeddings_matrix
{κ : Type w}
(A : Type u)
{B : Type v}
(C : Type z)
[comm_ring A]
[comm_ring B]
[algebra A B]
[comm_ring C]
[algebra A C]
(b : κ → B) :
embeddings_matrix 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.
def
algebra.embeddings_matrix_reindex
{κ : Type w}
(A : Type u)
{B : Type v}
(C : Type z)
[comm_ring A]
[comm_ring B]
[algebra A B]
[comm_ring C]
[algebra A C]
(b : κ → B)
(e : κ ≃ (B →ₐ[A] C)) :
matrix κ κ C
embeddings_matrix_reindex 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 := equiv_of_card_eq ((alg_hom.card A B C).trans h.symm).
Equations
- algebra.embeddings_matrix_reindex A C b e = ⇑(matrix.reindex (equiv.refl κ) e.symm) (algebra.embeddings_matrix A C b)
theorem
algebra.trace_matrix_eq_embeddings_matrix_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]
[is_separable K L]
[is_alg_closed E]
(b : κ → L) :
(algebra.trace_matrix K b).map ⇑(algebra_map K E) = (algebra.embeddings_matrix K E b).mul (algebra.embeddings_matrix K E b).transpose
theorem
algebra.trace_matrix_eq_embeddings_matrix_reindex_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]
[is_separable K L]
[is_alg_closed E]
(b : κ → L)
[fintype κ]
(e : κ ≃ (L →ₐ[K] E)) :
(algebra.trace_matrix K b).map ⇑(algebra_map K E) = (algebra.embeddings_matrix_reindex K E b e).mul (algebra.embeddings_matrix_reindex K E b e).transpose
theorem
det_trace_matrix_ne_zero'
{K : Type u_4}
{L : Type u_5}
[field K]
[field L]
[algebra K L]
(pb : power_basis K L)
[is_separable K L] :
(algebra.trace_matrix K ⇑(pb.basis)).det ≠ 0
theorem
det_trace_form_ne_zero
{K : Type u_4}
{L : Type u_5}
[field K]
[field L]
[algebra K L]
{ι : Type w}
[fintype ι]
[is_separable K L]
[decidable_eq ι]
(b : basis ι K L) :
(⇑(bilin_form.to_matrix b) (algebra.trace_form K L)).det ≠ 0
theorem
trace_form_nondegenerate
(K : Type u_4)
(L : Type u_5)
[field K]
[field L]
[algebra K L]
[finite_dimensional K L]
[is_separable K L] :