English
The matrix left-multiplication map commutes with localization: mapping left multiplication by a in S to the localized setting yields the expected leftMulMatrix in the localized basis.
Русский
Матрица левого умножения совместима с локализацией: отображение левого умножения на a в локализованной системе даёт ожидаемую матрицу leftMulMatrix в локализованном базисе.
LaTeX
$$$(algebraMap R R_m).mapMatrix (leftMulMatrix b a) = leftMulMatrix (b.localizationLocalization R_m M S_m) (algebraMap S S_m a)$$$
Lean4
theorem map_leftMulMatrix_localization {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι R S) (a : S) :
(algebraMap R Rₘ).mapMatrix (leftMulMatrix b a) =
leftMulMatrix (b.localizationLocalization Rₘ M Sₘ) (algebraMap S Sₘ a) :=
by
ext i j
simp only [Matrix.map_apply, RingHom.mapMatrix_apply, leftMulMatrix_eq_repr_mul, ← map_mul,
Basis.localizationLocalization_apply, Basis.localizationLocalization_repr_algebraMap]
