English
For g₁ and g₂ localized maps and a linear l, the restriction of scalars of the map equals the composition with iso maps, i.e., the equation in the statement.
Русский
Для г1 и г2 локализованных отображений и линейного l, ограничение скаляров отображения равно композиции с изоморфизмами, как в утверждении.
LaTeX
$$$(\\text{map } S l).restrictScalars R = (\\mathrm{IsLocalizedModule.iso} S g_2)^{-1} \\circ (\\text{IsLocalizedModule.map } S g_1 g_2 l) \\circ (\\mathrm{IsLocalizedModule.iso } S g_1)$$$
Lean4
theorem restrictScalars_map_eq {M' N' : Type*} [AddCommMonoid M'] [AddCommMonoid N'] [Module R M'] [Module R N']
(g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N') [IsLocalizedModule S g₁] [IsLocalizedModule S g₂] (l : M →ₗ[R] N) :
(map S l).restrictScalars R =
(IsLocalizedModule.iso S g₂).symm ∘ₗ IsLocalizedModule.map S g₁ g₂ l ∘ₗ IsLocalizedModule.iso S g₁ :=
by
rw [LinearEquiv.eq_toLinearMap_symm_comp, ← LinearEquiv.comp_toLinearMap_symm_eq]
apply IsLocalizedModule.linearMap_ext S g₁ g₂
rw [LinearMap.comp_assoc, IsLocalizedModule.iso_symm_comp]
ext
simp
