English
For m in span_R(range b) and i ∈ ι, the algebra map of the i-th coordinate of the restricted-repr equals the i-th coordinate of the original repr: algebraMap_R_S((b.restrictScalars R).repr m i) = b.repr m i.
Русский
Для m из span_R(range b) и i из ι, алгебраическое отображение координаты ограниченного представления равно соответствующей координате исходного представления: algebraMap_R_S((b.restrictScalars R).repr m i) = b.repr m i.
LaTeX
$$$\\ algebraMap_R_S\\left((b.restrictScalars R).\\mathrm{repr}\\, m\\, i\\right) = b.\\mathrm{repr}\\, m\\, i$$$
Lean4
@[simp]
theorem restrictScalars_repr_apply (m : span R (Set.range b)) (i : ι) :
algebraMap R S ((b.restrictScalars R).repr m i) = b.repr m i :=
by
suffices
Finsupp.mapRange.linearMap (Algebra.linearMap R S) ∘ₗ (b.restrictScalars R).repr.toLinearMap =
((b.repr : M →ₗ[S] ι →₀ S).restrictScalars R).domRestrict _
by exact DFunLike.congr_fun (LinearMap.congr_fun this m) i
refine Basis.ext (b.restrictScalars R) fun _ => ?_
simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_one, Basis.repr_self,
Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply, LinearMap.domRestrict_apply,
Basis.restrictScalars_apply, LinearMap.coe_restrictScalars]
