The trace along a tower of scalars #
Let A be a commutative R-algebra that is free as an R-module, and let M be a free
A-module. An A-linear endomorphism f of M has a trace over A, and, viewed as an
R-linear endomorphism, a trace over R. The second is the algebra trace from A to R of the
first. This is the module version of the transitivity of the algebra trace
Algebra.trace_trace_of_basis, and the additive counterpart of LinearMap.det_restrictScalars.
Main results #
LinearMap.trace_restrictScalars:tr_R(f) = Tr_{A/R}(tr_A(f)).
theorem
LinearMap.trace_restrictScalars
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[CommRing R]
[CommRing A]
[Algebra R A]
[Module.Free R A]
[AddCommMonoid M]
[Module R M]
[Module A M]
[IsScalarTower R A M]
[Module.Free A M]
(f : M →ₗ[A] M)
:
The trace along a tower of scalars. For a free A-module M, where A is a free
R-algebra, the R-trace of an A-linear endomorphism is the algebra trace of its A-trace.