# mathlib3documentation

algebra.module.localized_module

# Localized Module #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• `localized_module.r` : the equivalence relation defining this localization, namely `(m, s) ≈ (m', s')` if and only if if there is some `u : S` such that `u • s' • m = u • s • m'`.
• `localized_module M S` : the localized module by `S`.
• `localized_module.mk` : the canonical map sending `(m, s) : M × S ↦ m/s : localized_module M S`
• `localized_module.lift_on` : any well defined function `f : M × S → α` respecting `r` descents to a function `localized_module M S → α`
• `localized_module.lift_on₂` : any well defined function `f : M × S → M × S → α` respecting `r` descents to a function `localized_module M S → localized_module M S`
• `localized_module.mk_add_mk` : in the localized module `mk m s + mk m' s' = mk (s' • m + s • m') (s * s')`
• `localized_module.mk_smul_mk` : in the localized module, for any `r : R`, `s t : S`, `m : M`, we have `mk r s • mk m t = mk (r • m) (s * t)` where `mk r s : localization S` is localized ring by `S`.
• `localized_module.is_module` : `localized_module M S` is a `localization S`-module.

## Future work #

• Redefine `localization` for monoids and rings to coincide with `localized_module`.
def localized_module.r {R : Type u} (S : submonoid R) (M : Type v) [ M] (a b : 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
theorem localized_module.r.is_equiv {R : Type u} (S : submonoid R) (M : Type v) [ M] :
is_equiv (M × S) M)
@[protected, instance]
def localized_module.r.setoid {R : Type u} (S : submonoid R) (M : Type v) [ M] :
Equations
@[nolint]
def localized_module {R : Type u} (S : submonoid R) (M : Type v) [ M] :
Type (max u v)

If `S` is a multiplicative subset of a ring `R` and `M` an `R`-module, then we can localize `M` by `S`.

Equations
Instances for `localized_module`
def localized_module.mk {R : Type u} {S : submonoid R} {M : Type v} [ M] (m : M) (s : S) :

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

Equations
theorem localized_module.mk_eq {R : Type u} {S : submonoid R} {M : Type v} [ M] {m m' : M} {s s' : S} :
= s' (u : S), u s' m = u s m'
theorem localized_module.induction_on {R : Type u} {S : submonoid R} {M : Type v} [ M] {β : Prop} (h : (m : M) (s : S), β s)) (x : M) :
β x
theorem localized_module.induction_on₂ {R : Type u} {S : submonoid R} {M : Type v} [ M] {β : Prop} (h : (m m' : M) (s s' : S), β s) s')) (x y : M) :
β x y
def localized_module.lift_on {R : Type u} {S : submonoid R} {M : Type v} [ M] {α : Type u_1} (x : 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} {S : submonoid R} {M : Type v} [ M] {α : Type u_1} {f : M × S α} (wd : (p p' : M × S), p p' f p = f p') (m : M) (s : S) :
s).lift_on f wd = f (m, s)
def localized_module.lift_on₂ {R : Type u} {S : submonoid R} {M : Type v} [ M] {α : Type u_1} (x y : 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} {S : submonoid R} {M : Type v} [ 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) :
s).lift_on₂ s') f wd = f (m, s) (m', s')
@[protected, instance]
def localized_module.has_zero {R : Type u} {S : submonoid R} {M : Type v} [ M] :
Equations
@[simp]
theorem localized_module.zero_mk {R : Type u} {S : submonoid R} {M : Type v} [ M] (s : S) :
= 0
@[protected, instance]
def localized_module.has_add {R : Type u} {S : submonoid R} {M : Type v} [ M] :
Equations
theorem localized_module.mk_add_mk {R : Type u} {S : submonoid R} {M : Type v} [ M] {m1 m2 : M} {s1 s2 : S} :
s1 + s2 = localized_module.mk (s2 m1 + s1 m2) (s1 * s2)
@[protected, instance]
def localized_module.has_nat_smul {R : Type u} {S : submonoid R} {M : Type v} [ M] :
M)
Equations
@[protected, instance]
def localized_module.add_comm_monoid {R : Type u} {S : submonoid R} {M : Type v} [ M] :
Equations
@[protected, instance]
def localized_module.add_comm_group {R : Type u} {S : submonoid R} {M : Type u_1} [ M] :
Equations
theorem localized_module.mk_neg {R : Type u} {S : submonoid R} {M : Type u_1} [ M] {m : M} {s : S} :
@[protected, instance]
def localized_module.semiring {R : Type u} {A : Type u_1} [semiring A] [ A] {S : submonoid R} :
Equations
@[protected, instance]
def localized_module.ring {R : Type u} {A : Type u_1} [ring A] [ A] {S : submonoid R} :
ring A)
Equations
theorem localized_module.mk_mul_mk {R : Type u} {S : submonoid R} {A : Type u_1} [semiring A] [ A] {a₁ a₂ : A} {s₁ s₂ : S} :
s₁ * s₂ = localized_module.mk (a₁ * a₂) (s₁ * s₂)
@[protected, instance]
def localized_module.has_smul {R : Type u} {S : submonoid R} {M : Type v} [ M] :
M)
Equations
theorem localized_module.mk_smul_mk {R : Type u} {S : submonoid R} {M : Type v} [ M] (r : R) (m : M) (s t : S) :
= localized_module.mk (r m) (s * t)
@[protected, instance]
def localized_module.is_module {R : Type u} {S : submonoid R} {M : Type v} [ M] :
M)
Equations
@[simp]
theorem localized_module.mk_cancel_common_left {R : Type u} {S : submonoid R} {M : Type v} [ M] (s' s : S) (m : M) :
localized_module.mk (s' m) (s' * s) =
@[simp]
theorem localized_module.mk_cancel {R : Type u} {S : submonoid R} {M : Type v} [ M] (s : S) (m : M) :
@[simp]
theorem localized_module.mk_cancel_common_right {R : Type u} {S : submonoid R} {M : Type v} [ M] (s s' : S) (m : M) :
localized_module.mk (s' m) (s * s') =
@[protected, instance]
def localized_module.is_module' {R : Type u} {S : submonoid R} {M : Type v} [ M] :
M)
Equations
theorem localized_module.smul'_mk {R : Type u} {S : submonoid R} {M : Type v} [ M] (r : R) (s : S) (m : M) :
@[protected, instance]
def localized_module.algebra {R : Type u} {S : submonoid R} {A : Type u_1} [semiring A] [ A] :
A)
Equations
theorem localized_module.algebra_map_mk {R : Type u} {S : submonoid R} {A : Type u_1} [semiring A] [ A] (a : R) (s : S) :
A)) s) = localized_module.mk ( A) a) s
@[protected, instance]
def localized_module.is_scalar_tower {R : Type u} {S : submonoid R} {M : Type v} [ M] :
M)
@[protected, instance]
def localized_module.algebra' {R : Type u} {S : submonoid R} {A : Type u_1} [semiring A] [ A] :
A)
Equations
def localized_module.mk_linear_map {R : Type u} (S : submonoid R) (M : Type v) [ M] :

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

Equations
Instances for `localized_module.mk_linear_map`
@[simp]
theorem localized_module.mk_linear_map_apply {R : Type u} (S : submonoid R) (M : Type v) [ M] (m : M) :
def localized_module.div_by {R : Type u} {S : submonoid R} {M : Type v} [ M] (s : S) :

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} {S : submonoid R} {M : Type v} [ M] (s : S) (p : M) :
= p.lift_on (λ (p : M × S), (s * p.snd)) _
theorem localized_module.div_by_mul_by {R : Type u} {S : submonoid R} {M : Type v} [ M] (s : S) (p : M) :
(( M))) s) p) = p
theorem localized_module.mul_by_div_by {R : Type u} {S : submonoid R} {M : Type v} [ M] (s : S) (p : M) :
( M))) s) p) = p
@[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'] [ M] [ 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''] [ M] [ M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) :
M''

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''] [ M] [ M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) (m : M) (s : S) :
s) = ((_.unit)⁻¹.val) (g m)
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''] [ M] [ M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) (x y : M) :
(x + y) = x + y
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''] [ M] [ M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) (r : R) (m : M) :
r m = (r 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''] [ M] [ M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) :
→ₗ[R] M''

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''] [ M] [ M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) (m : M) (s : S) :
h) s) = ((_.unit)⁻¹.val) (g m)

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''] [ M] [ M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) :
h).comp = g

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''] [ M] [ M''] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) (l : →ₗ[R] M'') (hl : = g) :
= l

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`

@[protected, instance]
def localized_module_is_localized_module {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} [ M] :
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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] :
M'

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

Equations
@[simp]
theorem is_localized_module.from_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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) (s : S) :
= (_.unit)⁻¹ (f m)
theorem is_localized_module.from_localized_module'_add {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (x y : M) :
theorem is_localized_module.from_localized_module'_smul {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (r : R) (x : M) :
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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] :

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

Equations
theorem is_localized_module.from_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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) (s : S) :
= (_.unit)⁻¹ (f m)
theorem is_localized_module.from_localized_module.inj {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] :
theorem is_localized_module.from_localized_module.surj {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] :
theorem is_localized_module.from_localized_module.bij {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] :
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'] [ M] [ M'] (f : M →ₗ[R] M') [ 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_symm_apply {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (ᾰ : M') :
f).symm) =
@[simp]
theorem is_localized_module.iso_apply {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (ᾰ : M) :
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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) (s : S) :
s) = (_.unit)⁻¹ (f m)
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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M') :
f).symm) 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M') (a : M) (b : S) (eq1 : b m = f a) :
f).symm) m =
theorem is_localized_module.iso_symm_comp {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] :
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''] [ M] [ M'] [ M''] (f : M →ₗ[R] M') [ f] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( 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''] [ M] [ M'] [ M''] (f : M →ₗ[R] M') [ f] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) :
g h).comp f = g
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''] [ M] [ M'] [ M''] (f : M →ₗ[R] M') [ f] (g : M →ₗ[R] M'') (h : (x : S), is_unit ( M'')) x)) (l : M' →ₗ[R] M'') (hl : l.comp f = g) :
h = l
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''] [ M] [ M'] [ M''] (f : M →ₗ[R] M') [ f] (g : M →ₗ[R] M'') (map_unit : (x : S), is_unit ( 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''] [ M] [ M'] [ M''] (f : M →ₗ[R] M') [ f] (map_unit : (x : S), is_unit ( 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''] [ M] [ M'] [ M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [ f] [ 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'] [ M] [ M'] (f : M →ₗ[R] M') [ 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'] [ M] [ M'] (f : M →ₗ[R] M') [ 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'] [ M] [ M'] (f : M →ₗ[R] M') [ 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (r : R) (m : M) (s : S) :
(r m) s = r
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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m₁ m₂ : M) (s₁ s₂ : S) :
s₁ + s₂ = (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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (s : S) :
= 0
@[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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) :
= f 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) (s : S) :
(s m) s = f 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) (s : S) :
s = f m
@[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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) (s₁ s₂ : S) :
(s₁ m) (s₁ * s₂) = 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) (s₁ s₂ : S) :
(s₂ m) (s₁ * s₂) = 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m₁ m₂ : M) (s : S) :
(m₁ + m₂) s = 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m₁ m₂ : M) (s₁ s₂ : S) :
s₁ = 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m : M) (s : 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m₁ m₂ : M) (s : S) :
(m₁ - m₂) s = 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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] (m₁ m₂ : M) (s₁ s₂ : S) :
s₁ - s₂ = (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'] [ M] [ M'] (f : M →ₗ[R] M') (hf : (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂) [ f] (m₁ m₂ : M) (s₁ s₂ : S) :
s₁ * s₂ = (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'] [ M] [ M'] (f : M →ₐ[R] M') (m₁ m₂ : M) (s₁ s₂ : S) :
= (m₁ * m₂) (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'] [ M] [ M'] {f : M →ₗ[R] M'} [ f] {m : M} {s : S} {m' : M'} :
= m' f m = s 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'] [ M] [ M'] {f : M →ₗ[R] M'} [ f] {m : M} (s : S) :
= 0 f m = 0
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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] {m : M} (s : S) :
= 0 (s' : S), s' m = 0
theorem is_localized_module.mk_eq_mk' {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} [ M] (s : S) (m : M) :
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'] [ M] [ M'] (f : M →ₗ[R] M') [ f] {m : M} :
f m = 0 (s' : S), s' m = 0
theorem is_localized_module.mk'_surjective {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} {M' : Type u_3} [add_comm_monoid M'] [ M] [ M'] (f : M →ₗ[R] M') [ f] :
theorem is_localized_module.mk_of_algebra {R : Type u_1} {S : Type u_2} {S' : Type u_3} [comm_ring R] [comm_ring S] [comm_ring S'] [ S] [ S'] (M : submonoid R) (f : S →ₐ[R] S') (h₁ : (x : R), x M is_unit ( S') x)) (h₂ : (y : S'), (x : S × M), x.snd y = f x.fst) (h₃ : (x : S), f x = 0 ( (m : M), m x = 0)) :