English
More generally, the localization of the span of any set under f equals the span of the image of that set under f, viewed inside the localized module.
Русский
В более общем виде локализация порождающего множества по отображению f равна порождению образа этого множества под f в локализованном модуле.
LaTeX
$$$\\operatorname{localized}'(S,p,f)(\\operatorname{span}_R(T)) = \\operatorname{span}_S\\big(\\operatorname{Set.image}(f, T)\\big).$$$
Lean4
theorem localized₀_smul (I : Submodule R R) : (I • M').localized₀ p f = I • M'.localized₀ p f :=
by
apply le_antisymm
· rintro _ ⟨a, ha, s, rfl⟩
refine Submodule.smul_induction_on ha ?_ ?_
· intro r hr n hn
rw [IsLocalizedModule.mk'_smul]
exact Submodule.smul_mem_smul hr ⟨n, hn, s, rfl⟩
· simp +contextual only [IsLocalizedModule.mk'_add, add_mem, implies_true]
· refine Submodule.smul_le.mpr ?_
rintro r hr _ ⟨a, ha, s, rfl⟩
rw [← IsLocalizedModule.mk'_smul]
exact ⟨_, Submodule.smul_mem_smul hr ha, s, rfl⟩
