mathlib3 documentation

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 #

Future work #

source
def localized_module.r {R : Type u} [comm_semiring R] (S : submonoid R) (M : Type v) [add_comm_monoid M] [module R 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
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
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
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
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
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
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
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
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
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
source
@[protected, instance]
def localized_module.add_comm_group {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type u_1} [add_comm_group M] [module R M] :
add_comm_group (localized_module S M)
Equations
source
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} :
localized_module.mk (-m) s = -localized_module.mk m s
source
@[protected, instance]
def localized_module.semiring {R : Type u} [comm_semiring R] {A : Type u_1} [semiring A] [algebra R A] {S : submonoid R} :
semiring (localized_module S A)
Equations
source
@[protected, instance]
def localized_module.comm_semiring {R : Type u} [comm_semiring R] {A : Type u_1} [comm_semiring A] [algebra R A] {S : submonoid R} :
comm_semiring (localized_module S A)
Equations
source
@[protected, instance]
def localized_module.ring {R : Type u} [comm_semiring R] {A : Type u_1} [ring A] [algebra R A] {S : submonoid R} :
ring (localized_module S A)
Equations
source
@[protected, instance]
def localized_module.comm_ring {R : Type u} [comm_semiring R] {A : Type u_1} [comm_ring A] [algebra R A] {S : submonoid R} :
comm_ring (localized_module S A)
Equations
source
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₂)
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
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
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
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
@[protected, instance]
def localized_module.algebra {R : Type u} [comm_semiring R] {S : submonoid R} {A : Type u_1} [semiring A] [algebra R A] :
algebra (localization S) (localized_module S A)
Equations
source
theorem localized_module.algebra_map_mk {R : Type u} [comm_semiring R] {S : submonoid R} {A : Type u_1} [semiring A] [algebra R A] (a : R) (s : ↥S) :
⇑(algebra_map (localization S) (localized_module S A)) (localization.mk a s) = localized_module.mk (⇑(algebra_map R A) a) s
source
@[protected, instance]
def localized_module.is_scalar_tower {R : Type u} [comm_semiring R] {S : submonoid R} {M : Type v} [add_comm_monoid M] [module R M] :
is_scalar_tower R (localization S) (localized_module S M)
source
@[protected, instance]
def localized_module.algebra' {R : Type u} [comm_semiring R] {S : submonoid R} {A : Type u_1} [semiring A] [algebra R A] :
algebra R (localized_module S A)
Equations
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
Instances for localized_module.mk_linear_map
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
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_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
source
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)) :
localized_module S M → 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
source
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) :
localized_module.lift' S g h (localized_module.mk m s) = ⇑((_.unit)⁻¹.val) (⇑g m)
source
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) :
localized_module.lift' S g h (x + y) = localized_module.lift' S g h x + localized_module.lift' S g h y
source
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) :
r • localized_module.lift' S g h m = localized_module.lift' S g h (r • m)
source
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)) :
localized_module S M →ₗ[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
source
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) :
⇑(localized_module.lift S g h) (localized_module.mk m 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.

source
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)) :
(localized_module.lift S g h).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, then there is a linear map lift g ∘ mk_linear_map = g.

source
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) :
localized_module.lift S g h = 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

source
@[protected, instance]
def localized_module_is_localized_module {R : Type u_1} [comm_ring R] (S : submonoid R) {M : Type u_2} [add_comm_monoid M] [module R M] :
is_localized_module S (localized_module.mk_linear_map S M)
source
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] :
localized_module S M → M'

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

Equations
source
@[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] [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.from_localized_module' S f (localized_module.mk m s) = ⇑(_.unit)⁻¹ (⇑f m)
source
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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (x y : localized_module S M) :
is_localized_module.from_localized_module' S f (x + y) = is_localized_module.from_localized_module' S f x + is_localized_module.from_localized_module' S f y
source
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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (r : R) (x : localized_module S M) :
r • is_localized_module.from_localized_module' S f x = is_localized_module.from_localized_module' S f (r • x)
source
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] :
localized_module S M →ₗ[R] M'

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

Equations
source
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] [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.from_localized_module S f) (localized_module.mk m s) = ⇑(_.unit)⁻¹ (⇑f m)
source
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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] :
function.injective ⇑(is_localized_module.from_localized_module S f)
source
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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] :
function.surjective ⇑(is_localized_module.from_localized_module S f)
source
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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] :
function.bijective ⇑(is_localized_module.from_localized_module S f)
source
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] :
localized_module S M ≃ₗ[R] M'

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
source
@[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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (ᾰ : M') :
⇑((is_localized_module.iso S f).symm) ᾰ = (equiv.of_bijective ⇑(is_localized_module.from_localized_module S f) _).inv_fun ᾰ
source
@[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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] (ᾰ : localized_module S M) :
⇑(is_localized_module.iso S f) ᾰ = (is_localized_module.from_localized_module S f).to_fun ᾰ
source
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) :
⇑(is_localized_module.iso S f) (localized_module.mk m s) = ⇑(_.unit)⁻¹ (⇑f m)
source
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') :
⇑((is_localized_module.iso S f).symm) m = localized_module.mk _.some.fst _.some.snd
source
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) :
⇑((is_localized_module.iso S f).symm) m = localized_module.mk a b
source
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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] :
(is_localized_module.iso S f).symm.to_linear_map.comp f = localized_module.mk_linear_map S M
source
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
source
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)) :
(is_localized_module.lift S f g h).comp f = g
source
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) :
is_localized_module.lift S f g h = l
source
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''
source
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
source
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
source
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)
source
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₂
source
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
source
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) :
is_localized_module.mk' f (r • m) s = r • is_localized_module.mk' f m s
source
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₂)
source
@[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) :
is_localized_module.mk' f 0 s = 0
source
@[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) :
is_localized_module.mk' f m 1 = ⇑f m
source
@[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) :
is_localized_module.mk' f (s • m) s = ⇑f m
source
@[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) :
s • is_localized_module.mk' f m s = ⇑f m
source
@[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₂
source
@[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₁
source
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) :
is_localized_module.mk' f (m₁ + m₂) s = is_localized_module.mk' f m₁ s + is_localized_module.mk' f m₂ s
source
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₁
source
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) :
is_localized_module.mk' f (-m) s = -is_localized_module.mk' f m s
source
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) :
is_localized_module.mk' f (m₁ - m₂) s = is_localized_module.mk' f m₁ s - is_localized_module.mk' f m₂ s
source
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₂)
source
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₂)
source
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) :
is_localized_module.mk' f.to_linear_map m₁ s₁ * is_localized_module.mk' f.to_linear_map m₂ s₂ = is_localized_module.mk' f.to_linear_map (m₁ * m₂) (s₁ * s₂)
source
@[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'} :
is_localized_module.mk' f m s = m' ↔ ⇑f m = s • m'
source
@[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) :
is_localized_module.mk' f m s = 0 ↔ ⇑f m = 0
source
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
source
theorem is_localized_module.mk_eq_mk' {R : Type u_1} [comm_ring R] {S : submonoid R} {M : Type u_2} [add_comm_monoid M] [module R M] (s : ↥S) (m : M) :
localized_module.mk m s = is_localized_module.mk' (localized_module.mk_linear_map S M) m s
source
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
source
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] [add_comm_monoid M'] [module R M] [module R M'] (f : M →ₗ[R] M') [is_localized_module S f] :
function.surjective (function.uncurry (is_localized_module.mk' f))
source
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'] [algebra R S] [algebra R S'] (M : submonoid R) (f : S →ₐ[R] S') (h₁ : ∀ (x : R), x ∈ M → is_unit (⇑(algebra_map R 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)) :
is_localized_module M f.to_linear_map