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.

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

Implementation notes

Typically, the trace is defined specifically for finite field extensions. The definition is as general as possible and the assumption 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.

References

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

noncomputable def Algebra.trace (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : S →ₗ[R] R

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 = LinearMap.trace R S ∘ₗ (Algebra.lmul R S).toLinearMap

theorem Algebra.trace_apply (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) : (Algebra.trace R S) x = (LinearMap.trace R S) ((Algebra.lmul R S) x)

theorem Algebra.trace_eq_zero_of_not_exists_basis (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (h : ¬∃ (s : Finset S), Nonempty (Basis { x : S // x ∈ s } R S)) : Algebra.trace R S = 0

theorem Algebra.trace_eq_matrix_trace {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Basis ι R S) (s : S) : (Algebra.trace R S) s = ((Algebra.leftMulMatrix b) s).trace

theorem Algebra.trace_algebraMap_of_basis {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} [Fintype ι] (b : Basis ι R S) (x : R) : (Algebra.trace R S) ((algebraMap 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_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [StrongRankCondition R] [Module.Free R S] (x : R) : (Algebra.trace R S) ((algebraMap R S) x) = Module.finrank R S • 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} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower 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} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type u_4} {κ : Type u_5} [Finite ι] [Finite κ] (b : Basis ι R S) (c : Basis κ S T) : Algebra.trace R S ∘ₗ ↑R (Algebra.trace S T) = Algebra.trace R T

@[simp]

theorem Algebra.trace_trace {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Module.Free R S] [Module.Finite R S] [Module.Free S T] [Module.Finite S T] (x : T) : (Algebra.trace R S) ((Algebra.trace S T) x) = (Algebra.trace R T) x

@[simp]

theorem Algebra.trace_comp_trace {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Module.Free R S] [Module.Finite R S] [Module.Free S T] [Module.Finite S T] : Algebra.trace R S ∘ₗ ↑R (Algebra.trace S T) = Algebra.trace R T

@[simp]

theorem Algebra.trace_prod_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing 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.1 + (Algebra.trace R T) x.2

theorem Algebra.trace_prod {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing 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.traceForm (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : LinearMap.BilinForm R S

The traceForm 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.traceForm R S = (Algebra.lmul R S).toLinearMap.compr₂ (Algebra.trace R S)

@[simp]

theorem Algebra.traceForm_apply (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) (y : S) : ((Algebra.traceForm R S) x) y = (Algebra.trace R S) (x * y)

theorem Algebra.traceForm_isSymm (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : (Algebra.traceForm R S).IsSymm

theorem Algebra.traceForm_toMatrix (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Basis ι R S) (i : ι) (j : ι) : (BilinForm.toMatrix b) (Algebra.traceForm R S) i j = (Algebra.trace R S) (b i * b j)