English
Let N be a localization of M via p and f, and M′ ≤ M. Then the localized₀ submodule of M′ in N consists of all images f(m)/s with m ∈ M′, s ∈ p.
Русский
Пусть N локализуется относительно p из M через f, и M′ является подмодулем M. Тогда Submodule.localized₀(M′) в N состоит из всех элементов f(m)/s с m ∈ M′, s ∈ p.
LaTeX
$$$\\operatorname{localized}_0(p,f,M') = \\{\,x\\in N : \\exists m\\in M',\\exists s\\in p,\\ \\mathrm{IsLocalizedModule.mk'} f m s = x\\}.$$$
Lean4
/-- Let `N` be a localization of an `R`-module `M` at `p`.
This is the localization of an `R`-submodule of `M` viewed as an `R`-submodule of `N`. -/
def localized₀ : Submodule R N
where
carrier := {x | ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x}
add_mem' := fun {x y} ⟨m, hm, s, hx⟩ ⟨n, hn, t, hy⟩ ↦
⟨t • m + s • n, add_mem (M'.smul_mem t hm) (M'.smul_mem s hn), s * t, by
rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']⟩
zero_mem' := ⟨0, zero_mem _, 1, by simp⟩
smul_mem' r
x := by
rintro ⟨m, hm, s, hx⟩
exact ⟨r • m, smul_mem M' _ hm, s, by rw [IsLocalizedModule.mk'_smul, hx]⟩
