mathlib documentation

algebra.module.localized_module

Localized Module #

Given a commutative ring R, a multiplicative subset S ⊆ R and an R-module M, we can localize M by S. This gives us a localization S-module.

Main definitions #

Future work #

def localized_module.r {R : Type u} [comm_semiring R] (S : submonoid R) (M : Type v) [add_comm_monoid M] [module R M] :
M × S M × S Prop

The equivalence relation on M × S where (m1, s1) ≈ (m2, s2) if and only if for some (u : S), u * (s2 • m1 - s1 • m2) = 0

Equations
@[protected, instance]
def localized_module.r.setoid {R : Type u} [comm_semiring R] (S : submonoid R) (M : Type v) [add_comm_monoid M] [module R M] :
Equations
def localized_module.mk {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (m : M) (s : S) :

The canonical map sending (m, s) ↦ m/s

Equations
theorem localized_module.mk_eq {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] {m m' : M} {s s' : S} :
theorem localized_module.induction_on {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] {β : localized_module S M Prop} (h : (m : M) (s : S), β (localized_module.mk m s)) (x : localized_module S M) :
β x
theorem localized_module.induction_on₂ {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] {β : localized_module S M localized_module S M Prop} (h : (m m' : M) (s s' : S), β (localized_module.mk m s) (localized_module.mk m' s')) (x y : localized_module S M) :
β x y
def localized_module.lift_on {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] {α : Type u_1} (x : localized_module S M) (f : M × S α) (wd : (p p' : M × S), p p' f p = f p') :
α

If f : M × S → α respects the equivalence relation localized_module.r, then f descents to a map localized_module M S → α.

Equations
theorem localized_module.lift_on_mk {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] {α : Type u_1} {f : M × S α} (wd : (p p' : M × S), p p' f p = f p') (m : M) (s : S) :
(localized_module.mk m s).lift_on f wd = f (m, s)
def localized_module.lift_on₂ {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] {α : Type u_1} (x y : localized_module S M) (f : M × S M × S α) (wd : (p q p' q' : M × S), p p' q q' f p q = f p' q') :
α

If f : M × S → M × S → α respects the equivalence relation localized_module.r, then f descents to a map localized_module M S → localized_module M S → α.

Equations
theorem localized_module.lift_on₂_mk {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] {α : Type u_1} (f : M × S M × S α) (wd : (p q p' q' : M × S), p p' q q' f p q = f p' q') (m m' : M) (s s' : S) :
(localized_module.mk m s).lift_on₂ (localized_module.mk m' s') f wd = f (m, s) (m', s')
@[protected, instance]
Equations
@[simp]
theorem localized_module.zero_mk {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (s : S) :
@[protected, instance]
Equations
theorem localized_module.mk_add_mk {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] {m1 m2 : M} {s1 s2 : S} :
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem localized_module.mk_neg {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type u_1} [add_comm_group M] [module R M] {m : M} {s : S} :
@[protected, instance]
def localized_module.semiring {R : Type u} [comm_semiring R] {A : Type u_1} [semiring A] [algebra R A] {S : submonoid R} :
Equations
@[protected, instance]
def localized_module.ring {R : Type u} [comm_semiring R] {A : Type u_1} [ring A] [algebra R A] {S : submonoid R} :
Equations
@[protected, instance]
Equations
theorem localized_module.mk_mul_mk {R : Type u} [comm_semiring R] {S : submonoid R} {A : Type u_1} [semiring A] [algebra R A] {a₁ a₂ : A} {s₁ s₂ : S} :
localized_module.mk a₁ s₁ * localized_module.mk a₂ s₂ = localized_module.mk (a₁ * a₂) (s₁ * s₂)
@[protected, instance]
Equations
theorem localized_module.mk_smul_mk {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (r : R) (m : M) (s t : S) :
@[simp]
theorem localized_module.mk_cancel_common_left {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (s' s : S) (m : M) :
@[simp]
theorem localized_module.mk_cancel {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (s : S) (m : M) :
@[simp]
theorem localized_module.mk_cancel_common_right {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (s s' : S) (m : M) :
theorem localized_module.smul'_mk {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (r : R) (s : S) (m : M) :
@[protected, instance]
Equations
@[protected, instance]

The function m ↦ m / 1 as an R-linear map.

Equations
Instances for localized_module.mk_linear_map

For any s : S, there is an R-linear map given by a/b ↦ a/(b*s).

Equations
@[simp]
theorem localized_module.div_by_apply {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (s : S) (p : localized_module S M) :
@[class]
structure is_localized_module {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') :
Prop

The characteristic predicate for localized module. is_localized_module S f describes that f : M ⟶ M' is the localization map identifying M' as localized_module S M.

Instances of this typeclass
noncomputable def localized_module.lift' {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M''] [module R M] [module R M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) :

If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then there is a linear map localized_module S M → M''.

Equations
theorem localized_module.lift'_mk {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M''] [module R M] [module R M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) (m : M) (s : S) :
theorem localized_module.lift'_add {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M''] [module R M] [module R M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) (x y : localized_module S M) :
theorem localized_module.lift'_smul {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M''] [module R M] [module R M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) (r : R) (m : localized_module S M) :
noncomputable def localized_module.lift {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M''] [module R M] [module R M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) :

If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then there is a linear map localized_module S M → M''.

Equations
theorem localized_module.lift_mk {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M''] [module R M] [module R M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) (m : M) (s : S) :

If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then lift g m s = s⁻¹ • g m.

theorem localized_module.lift_comp {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M''] [module R M] [module R M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) :

If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then there is a linear map lift g ∘ mk_linear_map = g.

theorem localized_module.lift_unique {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M''] [module R M] [module R M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) (l : localized_module S M →ₗ[R] M'') (hl : l.comp (localized_module.mk_linear_map S M) = g) :

If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible and l is another linear map localized_module S M ⟶ M'' such that l ∘ mk_linear_map = g then l = lift g

noncomputable def is_localized_module.from_localized_module' {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] :

If (M', f : M ⟶ M') satisfies universal property of localized module, there is a canonical map localized_module S M ⟶ M'.

Equations
@[simp]
noncomputable def is_localized_module.from_localized_module {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] :

If (M', f : M ⟶ M') satisfies universal property of localized module, there is a canonical map localized_module S M ⟶ M'.

Equations
noncomputable def is_localized_module.iso {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] :

If (M', f : M ⟶ M') satisfies universal property of localized module, then M' is isomorphic to localized_module S M as an R-module.

Equations
@[simp]
theorem is_localized_module.iso_apply_mk {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) (s : S) :
theorem is_localized_module.iso_symm_apply_aux {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M') :
theorem is_localized_module.iso_symm_apply' {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M') (a : M) (b : S) (eq1 : b m = f a) :
noncomputable def is_localized_module.lift {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M'] [add_comm_monoid M''] [module R M] [module R M'] [module R M''] (f : M →ₗ[R] M') [is_localized_module S f] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) :
M' →ₗ[R] M''

If M' is a localized module and g is a linear map M' → M'' such that all scalar multiplication by s : S is invertible, then there is a linear map M' → M''.

Equations
theorem is_localized_module.lift_comp {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M'] [add_comm_monoid M''] [module R M] [module R M'] [module R M''] (f : M →ₗ[R] M') [is_localized_module S f] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) :
theorem is_localized_module.lift_unique {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M'] [add_comm_monoid M''] [module R M] [module R M'] [module R M''] (f : M →ₗ[R] M') [is_localized_module S f] (g : M →ₗ[R] M'') (h : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) (l : M' →ₗ[R] M'') (hl : l.comp f = g) :
theorem is_localized_module.is_universal {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M'] [add_comm_monoid M''] [module R M] [module R M'] [module R M''] (f : M →ₗ[R] M') [is_localized_module S f] (g : M →ₗ[R] M'') (map_unit : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) :
∃! (l : M' →ₗ[R] M''), l.comp f = g

Universal property from localized module: If (M', f : M ⟶ M') is a localized module then it satisfies the following universal property: For every R-module M'' which every s : S-scalar multiplication is invertible and for every R-linear map g : M ⟶ M'', there is a unique R-linear map l : M' ⟶ M'' such that l ∘ f = g.

M -----f----> M'
|           /
|g       /
|     /   l
v   /
M''
theorem is_localized_module.ring_hom_ext {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M'] [add_comm_monoid M''] [module R M] [module R M'] [module R M''] (f : M →ₗ[R] M') [is_localized_module S f] (map_unit : (x : S), is_unit ((algebra_map R (module.End R M'')) x)) ⦃j k : M' →ₗ[R] M''⦄ (h : j.comp f = k.comp f) :
j = k
noncomputable def is_localized_module.linear_equiv {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [add_comm_monoid M] [add_comm_monoid M'] [add_comm_monoid M''] [module R M] [module R M'] [module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [is_localized_module S f] [is_localized_module S g] :
M' ≃ₗ[R] M''

If (M', f) and (M'', g) both satisfy universal property of localized module, then M', M'' are isomorphic as R-module

Equations
theorem is_localized_module.smul_injective {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (s : S) :
function.injective (λ (m : M'), s m)
theorem is_localized_module.smul_inj {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (s : S) (m₁ m₂ : M') :
s m₁ = s m₂ m₁ = m₂
noncomputable def is_localized_module.mk' {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) (s : S) :
M'

mk' f m s is the fraction m/s with respect to the localization map f.

Equations
theorem is_localized_module.mk'_smul {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (r : R) (m : M) (s : S) :
theorem is_localized_module.mk'_add_mk' {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m₁ m₂ : M) (s₁ s₂ : S) :
is_localized_module.mk' f m₁ s₁ + is_localized_module.mk' f m₂ s₂ = is_localized_module.mk' f (s₂ m₁ + s₁ m₂) (s₁ * s₂)
@[simp]
theorem is_localized_module.mk'_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (s : S) :
@[simp]
theorem is_localized_module.mk'_one {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) :
@[simp]
theorem is_localized_module.mk'_cancel {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) (s : S) :
@[simp]
theorem is_localized_module.mk'_cancel' {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) (s : S) :
@[simp]
theorem is_localized_module.mk'_cancel_left {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) (s₁ s₂ : S) :
is_localized_module.mk' f (s₁ m) (s₁ * s₂) = is_localized_module.mk' f m s₂
@[simp]
theorem is_localized_module.mk'_cancel_right {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) (s₁ s₂ : S) :
is_localized_module.mk' f (s₂ m) (s₁ * s₂) = is_localized_module.mk' f m s₁
theorem is_localized_module.mk'_add {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m₁ m₂ : M) (s : S) :
theorem is_localized_module.mk'_eq_mk'_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m₁ m₂ : M) (s₁ s₂ : S) :
is_localized_module.mk' f m₁ s₁ = is_localized_module.mk' f m₂ s₂ (s : S), s s₁ m₂ = s s₂ m₁
theorem is_localized_module.mk'_neg {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_group M] [add_comm_group M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m : M) (s : S) :
theorem is_localized_module.mk'_sub {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_group M] [add_comm_group M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m₁ m₂ : M) (s : S) :
theorem is_localized_module.mk'_sub_mk' {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_group M] [add_comm_group M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (m₁ m₂ : M) (s₁ s₂ : S) :
is_localized_module.mk' f m₁ s₁ - is_localized_module.mk' f m₂ s₂ = is_localized_module.mk' f (s₂ m₁ - s₁ m₂) (s₁ * s₂)
theorem is_localized_module.mk'_mul_mk'_of_map_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [semiring M] [semiring M'] [module R M] [algebra R M'] (f : M →ₗ[R] M') (hf : (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂) [is_localized_module S f] (m₁ m₂ : M) (s₁ s₂ : S) :
is_localized_module.mk' f m₁ s₁ * is_localized_module.mk' f m₂ s₂ = is_localized_module.mk' f (m₁ * m₂) (s₁ * s₂)
theorem is_localized_module.mk'_mul_mk' {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [semiring M] [semiring M'] [algebra R M] [algebra R M'] (f : M →ₐ[R] M') [is_localized_module S f.to_linear_map] (m₁ m₂ : M) (s₁ s₂ : S) :
@[simp]
theorem is_localized_module.mk'_eq_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] {f : M →ₗ[R] M'} [is_localized_module S f] {m : M} {s : S} {m' : M'} :
@[simp]
theorem is_localized_module.mk'_eq_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] {f : M →ₗ[R] M'} [is_localized_module S f] {m : M} (s : S) :
theorem is_localized_module.mk'_eq_zero' {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] {m : M} (s : S) :
is_localized_module.mk' f m s = 0 (s' : S), s' m = 0
theorem is_localized_module.eq_zero_iff {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] {m : M} :
f m = 0 (s' : S), s' m = 0