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 someu : S
such thatu • s' • m = u • s • m'
.localized_module M S
: the localized module byS
.localized_module.mk
: the canonical map sending(m, s) : M × S ↦ m/s : localized_module M S
localized_module.lift_on
: any well defined functionf : M × S → α
respectingr
descents to a functionlocalized_module M S → α
localized_module.lift_on₂
: any well defined functionf : M × S → M × S → α
respectingr
descents to a functionlocalized_module M S → localized_module M S
localized_module.mk_add_mk
: in the localized modulemk m s + mk m' s' = mk (s' • m + s • m') (s * s')
localized_module.mk_smul_mk
: in the localized module, for anyr : R
,s t : S
,m : M
, we havemk r s • mk m t = mk (r • m) (s * t)
wheremk r s : localization S
is localized ring byS
.localized_module.is_module
:localized_module M S
is alocalization S
-module.
Future work #
- Redefine
localization
for monoids and rings to coincide withlocalized_module
.
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
- localized_module.r.setoid S M = {r := localized_module.r S M _inst_3, iseqv := _}
If S
is a multiplicative subset of a ring R
and M
an R
-module, then
we can localize M
by S
.
Equations
- localized_module S M = quotient (localized_module.r.setoid S M)
The canonical map sending (m, s) ↦ m/s
Equations
- localized_module.mk m s = ⟦(m, s)⟧
If f : M × S → α
respects the equivalence relation localized_module.r
, then
f
descents to a map localized_module M S → α
.
Equations
- x.lift_on f wd = quotient.lift_on x f wd
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
- x.lift_on₂ y f wd = quotient.lift_on₂ x y f wd
Equations
Equations
- localized_module.add_comm_monoid = {add := has_add.add localized_module.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul localized_module.has_nat_smul, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
Equations
- localized_module.has_smul = {smul := λ (f : localization S) (x : localized_module S M), f.lift_on (λ (r : R) (s : ↥S), x.lift_on (λ (p : M × ↥S), localized_module.mk (r • p.fst) (s * p.snd)) _) _}
Equations
- localized_module.is_module = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul localized_module.has_smul}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
Equations
- localized_module.is_module' = {to_distrib_mul_action := module.to_distrib_mul_action (module.comp_hom (localized_module S M) (algebra_map R (localization S))), add_smul := _, zero_smul := _}
The function m ↦ m / 1
as an R
-linear map.
Equations
- localized_module.mk_linear_map S M = {to_fun := λ (m : M), localized_module.mk m 1, map_add' := _, map_smul' := _}
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
- localized_module.div_by s = {to_fun := λ (p : localized_module S M), p.lift_on (λ (p : M × ↥S), localized_module.mk p.fst (s * p.snd)) _, map_add' := _, map_smul' := _}
- map_units : ∀ (x : ↥S), is_unit (⇑(algebra_map R (module.End R M')) ↑x)
- surj : ∀ (y : M'), ∃ (x : M × ↥S), x.snd • y = ⇑f x.fst
- eq_iff_exists : ∀ {x₁ x₂ : M}, ⇑f x₁ = ⇑f x₂ ↔ ∃ (c : ↥S), c • x₂ = c • x₁
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
.