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.

source

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

localized_module.r S M (m1, s1) (m2, s2) = ∃ (u : ↥S), u • s1 • m2 = u • s2 • m1

source

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

is_equiv (M × ↥S) (localized_module.r S M)

source

@[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] :

setoid (M × ↥S)

Equations

localized_module.r.setoid S M = {r := localized_module.r S M _inst_3, iseqv := _}

source

@[nolint]

def localized_module {R : Type u} [comm_semiring R] (S : submonoid R) (M : Type v) [add_comm_monoid M] [module R 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

localized_module S M = quotient (localized_module.r.setoid S M)

Instances for localized_module

source

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) :

localized_module S M

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

Equations

localized_module.mk m s = ⟦(m, s)⟧

source

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} :

localized_module.mk m s = localized_module.mk m' s' ↔ ∃ (u : ↥S), u • s • m' = u • s' • m

source

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

source

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

source

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

x.lift_on f wd = quotient.lift_on x f wd

source

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)

source

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

x.lift_on₂ y f wd = quotient.lift_on₂ x y f wd

source

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')

source

@[protected, instance]

def localized_module.has_zero {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] :

has_zero (localized_module S M)

Equations

localized_module.has_zero = {zero := localized_module.mk 0 1}

source

@[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) :

localized_module.mk 0 s = 0

source

@[protected, instance]

def localized_module.has_add {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] :

has_add (localized_module S M)

Equations

localized_module.has_add = {add := λ (p1 p2 : localized_module S M), p1.lift_on₂ p2 (λ (x y : M × ↥S), localized_module.mk (y.snd • x.fst + x.snd • y.fst) (x.snd * y.snd)) localized_module.has_add._proof_1}

source

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} :

localized_module.mk m1 s1 + localized_module.mk m2 s2 = localized_module.mk (s2 • m1 + s1 • m2) (s1 * s2)

source

@[protected, instance]

def localized_module.has_nat_smul {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] :

has_smul ℕ (localized_module S M)

Equations

localized_module.has_nat_smul = {smul := λ (n : ℕ), nsmul_rec n}

source

@[protected, instance]

def localized_module.add_comm_monoid {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] :

add_comm_monoid (localized_module S M)

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 := _}

source

@[protected, instance]

def localized_module.has_smul {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] :

has_smul (localization S) (localized_module S M)

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)) _) _}

source

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) :

localization.mk r s • localized_module.mk m t = localized_module.mk (r • m) (s * t)

source

@[protected, instance]

def localized_module.is_module {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] :

module (localization S) (localized_module S M)

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 := _}

source

@[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) :

localized_module.mk (s' • m) (s' * s) = localized_module.mk m s

source

@[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) :

localized_module.mk (s • m) s = localized_module.mk m 1

source

@[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) :

localized_module.mk (s' • m) (s * s') = localized_module.mk m s

source

@[protected, instance]

def localized_module.is_module' {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] :

module R (localized_module S M)

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 := _}

source

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) :

r • localized_module.mk m s = localized_module.mk (r • m) s

source

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

M →ₗ[R] localized_module S M

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

localized_module_is_localized_module

source

@[simp]

theorem localized_module.mk_linear_map_apply {R : Type u} [comm_semiring R] (S : submonoid R) (M : Type v) [add_comm_monoid M] [module R M] (m : M) :

⇑(localized_module.mk_linear_map S M) m = localized_module.mk m 1

source

def localized_module.div_by {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] (s : ↥S) :

localized_module S M →ₗ[R] localized_module S M

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' := _}

source

@[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) :

⇑(localized_module.div_by s) p = p.lift_on (λ (p : M × ↥S), localized_module.mk p.fst (s * p.snd)) _

source

theorem localized_module.div_by_mul_by {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) :

⇑(localized_module.div_by s) (⇑(⇑(algebra_map R (module.End R (localized_module S M))) ↑s) p) = p

source

theorem localized_module.mul_by_div_by {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) :

⇑(⇑(algebra_map R (module.End R (localized_module S M))) ↑s) (⇑(localized_module.div_by s) p) = p

source

@[class]

structure is_localized_module {R : Type u} [comm_ring R] (S : submonoid R) {M M' : Type u} [add_comm_monoid M] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') :

Prop

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.

Instances of this typeclass

localized_module_is_localized_module

source

@[protected, instance]

def localized_module_is_localized_module {R : Type u} [comm_ring R] (S : submonoid R) {M : Type u} [add_comm_monoid M] [module R M] :

is_localized_module S (localized_module.mk_linear_map S M)