English
Relating the smul of localized' with restrictScalars shows compatibility of scalar restriction with the localized' construction.
Русский
Связь на умножение с ограничением скаляров показывает совместимость локализации localized' с ограничением скаляров.
LaTeX
$$$\\text{restrictScalars}_\\text{localized'}\\_smul = \\text{localized'}_\\text{smul}.$$$
Lean4
theorem restrictScalars_localized'_smul (I : Submodule R R) (N' : Submodule S N) :
(I.localized' S p (Algebra.linearMap R S) • N').restrictScalars R = I • N'.restrictScalars R :=
by
refine le_antisymm (fun x hx ↦ ?_) (Submodule.smul_le.mpr fun r hr n hn ↦ ?_)
· refine smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ fun _ _ ↦ add_mem
rintro _ ⟨r, hr, s, rfl⟩ n hn
rw [← IsLocalization.mk'_eq_mk', IsLocalization.mk'_eq_mul_mk'_one, mul_smul, algebraMap_smul]
exact smul_mem_smul hr ((Submodule.restrictScalars_mem _ _ _).mpr <| smul_mem _ _ hn)
· rw [← algebraMap_smul S, Submodule.restrictScalars_mem]
exact Submodule.smul_mem_smul ⟨_, hr, 1, by simp⟩ hn
