# Documentation

Mathlib.RingTheory.Trace

# 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

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

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