English
Let f be a linear endomorphism of a free finite R-module M and A a commutative ring with an algebra structure over R. then the trace after base change to A equals the algebra map of the trace over R applied to f.
Русский
Пусть f — линейное преобразование на свободном конечном модуле M над R; после базового изменения базы к A след равен образованию по алгебраическому отображению алгебры R в A от следа f.
LaTeX
$$$ \operatorname{trace}_A (f.baseChange A) = \operatorname{algebraMap}_{R}^{A} ( \operatorname{trace}_R M f ). $$$
Lean4
@[simp]
theorem trace_baseChange [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (A : Type*) [CommRing A] [Algebra R A] :
trace A _ (f.baseChange A) = algebraMap R A (trace R _ f) :=
by
let b := Module.Free.chooseBasis R M
let b' := Algebra.TensorProduct.basis A b
change _ = (algebraMap R A : R →+ A) _
simp [b', trace_eq_matrix_trace R b, trace_eq_matrix_trace A b', AddMonoidHom.map_trace]
