English
If b is a basis of S over R, then the trace matrix after localization equals the image, under the localization map, of the trace matrix of b over R.
Русский
Если b — база S как R-модуля, то матрица следа после локализации равна образу по локализационному отображению матрицы следа от b над R.
LaTeX
$$$\\operatorname{traceMatrix}_{R_m}(\\mathrm{Module.Basis.localizationLocalization\\,R_m\\,M\\,S_m\\, b}) = (\\mathrm{algebraMap}_R^{R_m}).mapMatrix (\\operatorname{traceMatrix}_R(b)).$$$
Lean4
theorem traceMatrix_localizationLocalization (b : Basis ι R S) :
Algebra.traceMatrix Rₘ (b.localizationLocalization Rₘ M Sₘ) =
(algebraMap R Rₘ).mapMatrix (Algebra.traceMatrix R b) :=
by
have : Module.Finite R S := Module.Finite.of_basis b
have : Module.Free R S := Module.Free.of_basis b
ext i j : 2
simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, traceMatrix_apply, traceForm_apply,
Basis.localizationLocalization_apply, ← map_mul]
exact Algebra.trace_localization R M _
