English
Let M be an R-module with basis b, and let S be a submonoid of R with R_s the localization. If f: M → M_s is R-linear and factors through localization, then for every m ∈ M and every i in the index set ι, the i-th coordinate of the localized representation of f(m) equals the image of the i-th coordinate of m under the canonical algebra hom R → R_s.
Русский
Пусть M — модуль над R с базисом b, S — подмножество моноида R, R_s — локализация, и f: M → M_s линейно над R и факторизуется через локализацию. Тогда для каждого m ∈ M и каждого i ∈ ι i‑й коэффициент представления f(m) в локализованном базисе равен образу i‑го коэффициента m по алгебраическому гомоморфизму R → R_s.
LaTeX
$$$ ((b.ofIsLocalizedModule R_s S f).repr (f m)) i = algebraMap R R_s (b.repr m i) $$$
Lean4
@[simp]
theorem ofIsLocalizedModule_repr_apply (m : M) (i : ι) :
((b.ofIsLocalizedModule Rₛ S f).repr (f m)) i = algebraMap R Rₛ (b.repr m i) :=
by
suffices
((b.ofIsLocalizedModule Rₛ S f).repr.toLinearMap.restrictScalars R) ∘ₗ f =
Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ b.repr.toLinearMap
by exact DFunLike.congr_fun (LinearMap.congr_fun this m) i
refine ext b fun i ↦ ?_
rw [LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, ←
b.ofIsLocalizedModule_apply Rₛ S f, repr_self, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe,
repr_self, Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply, map_one]
