English
The localized' submodule of N over S is the S-span of all images f(m) with m ∈ M′ and s ∈ p, viewed as an S-submodule of N.
Русский
Подмодуль localized' над S есть S-обобщение всех образов f(m) при m∈M′ и s∈p, рассмотренное как S-подмодуль N.
LaTeX
$$$\\operatorname{localized}'(S,p,f) = \\operatorname{span}_S\\{ \\mathrm{IsLocalizedModule.mk'} f m s : m\\in M',\\ s\\in p \\}.$$$
Lean4
/-- Let `S` be the localization of `R` at `p` and `N` be a localization of `M` at `p`.
This is the localization of an `R`-submodule of `M` viewed as an `S`-submodule of `N`. -/
def localized' : Submodule S N where
__ := localized₀ p f M'
smul_mem' := fun r x ⟨m, hm, s, hx⟩ ↦
by
have ⟨y, t, hyt⟩ := IsLocalization.mk'_surjective p r
exact ⟨y • m, M'.smul_mem y hm, t * s, by simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']⟩
