# mathlibdocumentation

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 #

• 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] :
M × SM × 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 × SM × 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 × SM × 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.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) :
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} [comm_ring R] (S : submonoid R) {M M' : Type u} [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
@[protected, instance]
def localized_module_is_localized_module {R : Type u} [comm_ring R] (S : submonoid R) {M : Type u} [ M] :