The regular trace form of a possibly noncommutative algebra

Mathlib's Algebra.trace and Algebra.traceForm are stated for commutative algebras. For an arbitrary R-algebra S, finite free over R, the regular trace of x is still the trace of left multiplication by x, and the regular trace form pairs x and y to the regular trace of x * y. This is the pairing used to bound orders in finite-dimensional algebras, such as group algebras and matrix algebras, by a dual lattice.

Main definitions

• Algebra.regularTraceForm R S: the bilinear form (x, y) ↦ Tr_R (z ↦ x * y * z).

Main results

• Algebra.regularTraceForm_eq_traceForm: for commutative S it is Algebra.traceForm R S.
• Algebra.isIntegral_trace_lmul: over a field K which is an R-algebra, the regular trace of an element integral over R is integral over R.

noncomputable def Algebra.regularTraceForm (R : Type u_1) (S : Type u_2) [CommRing R] [Ring S] [Algebra R S] : LinearMap.BilinForm R S

The regular trace form of an R-algebra S, which need not be commutative: it pairs x and y to the trace over R of left multiplication by x * y. For commutative S this is Algebra.traceForm R S (Algebra.regularTraceForm_eq_traceForm).

@[simp]

theorem Algebra.regularTraceForm_apply (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (x y : S) : ((regularTraceForm R S) x) y = (LinearMap.trace R S) ((lmul R S) (x * y))

theorem Algebra.regularTraceForm_eq_traceForm (R : Type u_1) [CommRing R] (S : Type u_3) [CommRing S] [Algebra R S] : regularTraceForm R S = traceForm R S

For a commutative algebra the regular trace form is Mathlib's trace form.

theorem Algebra.isIntegral_trace_lmul {R : Type u_3} {K : Type u_4} {E : Type u_5} [CommRing R] [Field K] [Ring E] [Algebra K E] [Algebra R K] [Algebra R E] [IsScalarTower R K E] [FiniteDimensional K E] {x : E} (hx : IsIntegral R x) : IsIntegral R ((LinearMap.trace K E) ((lmul K E) x))

The regular trace of an integral element is integral. Let K be a field which is an R-algebra and E a finite-dimensional K-algebra, not necessarily commutative. If x : E is integral over R, then so is the trace over K of left multiplication by x.