Localized Module

Given a commutative semiring 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

• LocalizedModule.r: the equivalence relation defining this localization, namely (m, s) ≈ (m', s') if and only if there is some u : S such that u • s' • m = u • s • m'.
• LocalizedModule M S: the localized module by S.
• LocalizedModule.mk: the canonical map sending (m, s) : M × S ↦ m/s : LocalizedModule M S
• LocalizedModule.liftOn: any well defined function f : M × S → α respecting r descents to a function LocalizedModule M S → α
• LocalizedModule.liftOn₂: any well defined function f : M × S → M × S → α respecting r descents to a function LocalizedModule M S → LocalizedModule M S
• LocalizedModule.mk_add_mk: in the localized module mk m s + mk m' s' = mk (s' • m + s • m') (s * s')
• LocalizedModule.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.
• LocalizedModule.isModule : LocalizedModule M S is a Localization S-module.

Future work

• Redefine Localization for monoids and rings to coincide with LocalizedModule.

def LocalizedModule.r {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] (a : M × ↥S) (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

• LocalizedModule.r S M a b = ∃ (u : ↥S), u • b.2 • a.1 = u • a.2 • b.1

theorem LocalizedModule.r.isEquiv {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] : IsEquiv (M × ↥S) (LocalizedModule.r S M)

instance LocalizedModule.r.setoid {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] : Setoid (M × ↥S)

Equations

• LocalizedModule.r.setoid S M = { r := LocalizedModule.r S M, iseqv := ⋯ }

def LocalizedModule {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid 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

• LocalizedModule S M = Quotient (LocalizedModule.r.setoid S M)

def LocalizedModule.mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (m : M) (s : ↥S) : LocalizedModule S M

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

Equations

• LocalizedModule.mk m s = Quotient.mk' (m, s)

theorem LocalizedModule.mk_eq {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {m : M} {m' : M} {s : ↥S} {s' : ↥S} : LocalizedModule.mk m s = LocalizedModule.mk m' s' ↔ ∃ (u : ↥S), u • s' • m = u • s • m'

theorem LocalizedModule.induction_on {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {β : LocalizedModule S M → Prop} (h : ∀ (m : M) (s : ↥S), β (LocalizedModule.mk m s)) (x : LocalizedModule S M) : β x

theorem LocalizedModule.induction_on₂ {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {β : LocalizedModule S M → LocalizedModule S M → Prop} (h : ∀ (m m' : M) (s s' : ↥S), β (LocalizedModule.mk m s) (LocalizedModule.mk m' s')) (x : LocalizedModule S M) (y : LocalizedModule S M) : β x y

def LocalizedModule.liftOn {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {α : Type u_2} (x : LocalizedModule S M) (f : M × ↥S → α) (wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p') : α

If f : M × S → α respects the equivalence relation LocalizedModule.r, then f descents to a map LocalizedModule M S → α.

Equations

• x.liftOn f wd = Quotient.liftOn x f wd

theorem LocalizedModule.liftOn_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {α : Type u_2} {f : M × ↥S → α} (wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p') (m : M) (s : ↥S) : (LocalizedModule.mk m s).liftOn f wd = f (m, s)

def LocalizedModule.liftOn₂ {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {α : Type u_2} (x : LocalizedModule S M) (y : LocalizedModule 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 LocalizedModule.r, then f descents to a map LocalizedModule M S → LocalizedModule M S → α.

Equations

• x.liftOn₂ y f wd = Quotient.liftOn₂ x y f wd

theorem LocalizedModule.liftOn₂_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {α : Type u_2} (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' : M) (s : ↥S) (s' : ↥S) : (LocalizedModule.mk m s).liftOn₂ (LocalizedModule.mk m' s') f wd = f (m, s) (m', s')

instance LocalizedModule.instZero {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] : Zero (LocalizedModule S M)

Equations

• LocalizedModule.instZero = { zero := LocalizedModule.mk 0 1 }

theorem LocalizedModule.subsingleton {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (h : 0 ∈ S) : Subsingleton (LocalizedModule S M)

If S contains 0 then the localization at S is trivial.

@[simp]

theorem LocalizedModule.zero_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : ↥S) : LocalizedModule.mk 0 s = 0

instance LocalizedModule.instAdd {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] : Add (LocalizedModule S M)

Equations

• LocalizedModule.instAdd = { add := fun (p1 p2 : LocalizedModule S M) => p1.liftOn₂ p2 (fun (x y : M × ↥S) => LocalizedModule.mk (y.2 • x.1 + x.2 • y.1) (x.2 * y.2)) ⋯ }

theorem LocalizedModule.mk_add_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {m1 : M} {m2 : M} {s1 : ↥S} {s2 : ↥S} : LocalizedModule.mk m1 s1 + LocalizedModule.mk m2 s2 = LocalizedModule.mk (s2 • m1 + s1 • m2) (s1 * s2)

instance LocalizedModule.hasNatSMul {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] : SMul ℕ (LocalizedModule S M)

Equations

• LocalizedModule.hasNatSMul = { smul := fun (n : ℕ) => nsmulRec n }

instance LocalizedModule.instAddCommMonoid {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] : AddCommMonoid (LocalizedModule S M)

Equations

• LocalizedModule.instAddCommMonoid = AddCommMonoid.mk ⋯

instance LocalizedModule.instNeg {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommGroup M] [Module R M] : Neg (LocalizedModule S M)

Equations

• LocalizedModule.instNeg = { neg := fun (p : LocalizedModule S M) => p.liftOn (fun (x : M × ↥S) => LocalizedModule.mk (-x.1) x.2) ⋯ }

instance LocalizedModule.instAddCommGroup {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommGroup M] [Module R M] : AddCommGroup (LocalizedModule S M)

Equations

• LocalizedModule.instAddCommGroup = AddCommGroup.mk ⋯

theorem LocalizedModule.mk_neg {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommGroup M] [Module R M] {m : M} {s : ↥S} : LocalizedModule.mk (-m) s = -LocalizedModule.mk m s

instance LocalizedModule.instMonoid {R : Type u} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {S : Submonoid R} : Monoid (LocalizedModule S A)

Equations

• LocalizedModule.instMonoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

instance LocalizedModule.instSemiring {R : Type u} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {S : Submonoid R} : Semiring (LocalizedModule S A)

Equations

• LocalizedModule.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

instance LocalizedModule.instCommSemiring {R : Type u} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] {S : Submonoid R} : CommSemiring (LocalizedModule S A)

Equations

• LocalizedModule.instCommSemiring = CommSemiring.mk ⋯

instance LocalizedModule.instRing {R : Type u} [CommSemiring R] {A : Type u_2} [Ring A] [Algebra R A] {S : Submonoid R} : Ring (LocalizedModule S A)

Equations

• LocalizedModule.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance LocalizedModule.instCommRing {R : Type u} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] {S : Submonoid R} : CommRing (LocalizedModule S A)

Equations

• LocalizedModule.instCommRing = CommRing.mk ⋯

theorem LocalizedModule.mk_mul_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {A : Type u_2} [Semiring A] [Algebra R A] {a₁ : A} {a₂ : A} {s₁ : ↥S} {s₂ : ↥S} : LocalizedModule.mk a₁ s₁ * LocalizedModule.mk a₂ s₂ = LocalizedModule.mk (a₁ * a₂) (s₁ * s₂)

noncomputable instance LocalizedModule.instSMul {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] : SMul T (LocalizedModule S M)

Equations

• One or more equations did not get rendered due to their size.

theorem LocalizedModule.smul_def {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] (x : T) (m : M) (s : ↥S) : x • LocalizedModule.mk m s = LocalizedModule.mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s)

theorem LocalizedModule.mk'_smul_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] (r : R) (m : M) (s : ↥S) (s' : ↥S) : IsLocalization.mk' T r s • LocalizedModule.mk m s' = LocalizedModule.mk (r • m) (s * s')

theorem LocalizedModule.mk_smul_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (m : M) (s : ↥S) (t : ↥S) : Localization.mk r s • LocalizedModule.mk m t = LocalizedModule.mk (r • m) (s * t)

noncomputable instance LocalizedModule.isModule {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {T : Type u_1} [CommSemiring T] [Algebra R T] [IsLocalization S T] : Module T (LocalizedModule S M)

Equations

• LocalizedModule.isModule = Module.mk ⋯ ⋯

@[simp]

theorem LocalizedModule.mk_cancel_common_left {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s' : ↥S) (s : ↥S) (m : M) : LocalizedModule.mk (s' • m) (s' * s) = LocalizedModule.mk m s

@[simp]

theorem LocalizedModule.mk_cancel {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : ↥S) (m : M) : LocalizedModule.mk (s • m) s = LocalizedModule.mk m 1

@[simp]

theorem LocalizedModule.mk_cancel_common_right {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : ↥S) (s' : ↥S) (m : M) : LocalizedModule.mk (s' • m) (s * s') = LocalizedModule.mk m s

noncomputable instance LocalizedModule.isModule' {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] : Module R (LocalizedModule S M)

Equations

• LocalizedModule.isModule' = Module.mk ⋯ ⋯

theorem LocalizedModule.smul'_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (s : ↥S) (m : M) : r • LocalizedModule.mk m s = LocalizedModule.mk (r • m) s

theorem LocalizedModule.smul_eq_iff_of_mem {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (hr : r ∈ S) (x : LocalizedModule S M) (y : LocalizedModule S M) : r • x = y ↔ x = Localization.mk 1 ⟨r, hr⟩ • y

theorem LocalizedModule.eq_zero_of_smul_eq_zero {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (r : R) (hr : r ∈ S) (x : LocalizedModule S M) (hx : r • x = 0) : x = 0

theorem LocalizedModule.smul'_mul {R : Type u} [CommSemiring R] {S : Submonoid R} {T : Type u_1} [CommSemiring T] [Algebra R T] [IsLocalization S T] {A : Type u_2} [Semiring A] [Algebra R A] (x : T) (p₁ : LocalizedModule S A) (p₂ : LocalizedModule S A) : x • p₁ * p₂ = x • (p₁ * p₂)

theorem LocalizedModule.mul_smul' {R : Type u} [CommSemiring R] {S : Submonoid R} {T : Type u_1} [CommSemiring T] [Algebra R T] [IsLocalization S T] {A : Type u_2} [Semiring A] [Algebra R A] (x : T) (p₁ : LocalizedModule S A) (p₂ : LocalizedModule S A) : p₁ * x • p₂ = x • (p₁ * p₂)

noncomputable instance LocalizedModule.instAlgebra {R : Type u} [CommSemiring R] {S : Submonoid R} (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] {A : Type u_2} [Semiring A] [Algebra R A] : Algebra T (LocalizedModule S A)

Equations

• LocalizedModule.instAlgebra T = Algebra.ofModule ⋯ ⋯

theorem LocalizedModule.algebraMap_mk' {R : Type u} [CommSemiring R] {S : Submonoid R} (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] {A : Type u_2} [Semiring A] [Algebra R A] (a : R) (s : ↥S) : (algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = LocalizedModule.mk ((algebraMap R A) a) s

theorem LocalizedModule.algebraMap_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {A : Type u_2} [Semiring A] [Algebra R A] (a : R) (s : ↥S) : (algebraMap (Localization S) (LocalizedModule S A)) (Localization.mk a s) = LocalizedModule.mk ((algebraMap R A) a) s

instance LocalizedModule.instIsScalarTower {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (T : Type u_1) [CommSemiring T] [Algebra R T] [IsLocalization S T] : IsScalarTower R T (LocalizedModule S M)

Equations

• ⋯ = ⋯

noncomputable instance LocalizedModule.algebra' {R : Type u} [CommSemiring R] {S : Submonoid R} {A : Type u_2} [Semiring A] [Algebra R A] : Algebra R (LocalizedModule S A)

Equations

• LocalizedModule.algebra' = Algebra.mk ((algebraMap (Localization S) (LocalizedModule S A)).comp (algebraMap R (Localization S))) ⋯ ⋯

@[simp]

theorem LocalizedModule.mkLinearMap_apply {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] (m : M) : (LocalizedModule.mkLinearMap S M) m = LocalizedModule.mk m 1

def LocalizedModule.mkLinearMap {R : Type u} [CommSemiring R] (S : Submonoid R) (M : Type v) [AddCommMonoid M] [Module R M] : M →ₗ[R] LocalizedModule S M

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

Equations

• LocalizedModule.mkLinearMap S M = { toFun := fun (m : M) => LocalizedModule.mk m 1, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LocalizedModule.divBy_apply {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : ↥S) (p : LocalizedModule S M) : (LocalizedModule.divBy s) p = p.liftOn (fun (p : M × ↥S) => LocalizedModule.mk p.1 (p.2 * s)) ⋯

def LocalizedModule.divBy {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : ↥S) : LocalizedModule S M →ₗ[R] LocalizedModule S M

For any s : S, there is an R-linear map given by a/b ↦ a/(b*s).

Equations

• LocalizedModule.divBy s = { toFun := fun (p : LocalizedModule S M) => p.liftOn (fun (p : M × ↥S) => LocalizedModule.mk p.1 (p.2 * s)) ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem LocalizedModule.divBy_mul_by {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : ↥S) (p : LocalizedModule S M) : (LocalizedModule.divBy s) (((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) p) = p

theorem LocalizedModule.mul_by_divBy {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] (s : ↥S) (p : LocalizedModule S M) : ((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) ((LocalizedModule.divBy s) p) = p

theorem isLocalizedModule_iff {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') : IsLocalizedModule S f ↔ (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M')) ↑x)) ∧ (∀ (y : M'), ∃ (x : M × ↥S), x.2 • y = f x.1) ∧ ∀ {x₁ x₂ : M}, f x₁ = f x₂ → ∃ (c : ↥S), c • x₁ = c • x₂

class IsLocalizedModule {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') : Prop

The characteristic predicate for localized module. IsLocalizedModule S f describes that f : M ⟶ M' is the localization map identifying M' as LocalizedModule S M.

• map_units : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M')) ↑x)
• surj' : ∀ (y : M'), ∃ (x : M × ↥S), x.2 • y = f x.1
• exists_of_eq : ∀ {x₁ x₂ : M}, f x₁ = f x₂ → ∃ (c : ↥S), c • x₁ = c • x₂

theorem IsLocalizedModule.map_units {R : Type u_1} : ∀ {inst : CommSemiring R} {S : Submonoid R} {M : Type u_2} {M' : Type u_3} {inst_1 : AddCommMonoid M} {inst_2 : AddCommMonoid M'} {inst_3 : Module R M} {inst_4 : Module R M'} (f : M →ₗ[R] M') [self : IsLocalizedModule S f] (x : ↥S), IsUnit ((algebraMap R (Module.End R M')) ↑x)

theorem IsLocalizedModule.surj' {R : Type u_1} : ∀ {inst : CommSemiring R} {S : Submonoid R} {M : Type u_2} {M' : Type u_3} {inst_1 : AddCommMonoid M} {inst_2 : AddCommMonoid M'} {inst_3 : Module R M} {inst_4 : Module R M'} {f : M →ₗ[R] M'} [self : IsLocalizedModule S f] (y : M'), ∃ (x : M × ↥S), x.2 • y = f x.1

theorem IsLocalizedModule.exists_of_eq {R : Type u_1} : ∀ {inst : CommSemiring R} {S : Submonoid R} {M : Type u_2} {M' : Type u_3} {inst_1 : AddCommMonoid M} {inst_2 : AddCommMonoid M'} {inst_3 : Module R M} {inst_4 : Module R M'} {f : M →ₗ[R] M'} [self : IsLocalizedModule S f] {x₁ x₂ : M}, f x₁ = f x₂ → ∃ (c : ↥S), c • x₁ = c • x₂

theorem IsLocalizedModule.surj {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (y : M') : ∃ (x : M × ↥S), x.2 • y = f x.1

theorem IsLocalizedModule.eq_iff_exists {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {x₁ : M} {x₂ : M} : f x₁ = f x₂ ↔ ∃ (c : ↥S), c • x₁ = c • x₂

theorem IsLocalizedModule.of_linearEquiv {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (e : M' ≃ₗ[R] M'') [hf : IsLocalizedModule S f] : IsLocalizedModule S (↑e ∘ₗ f)

theorem isLocalizedModule_id {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) [AddCommMonoid M] [Module R M] (R' : Type u_6) [CommSemiring R'] [Algebra R R'] [IsLocalization S R'] [Module R' M] [IsScalarTower R R' M] : IsLocalizedModule S LinearMap.id

theorem isLocalizedModule_iff_isLocalization {R : Type u_1} [CommSemiring R] {S : Submonoid R} {A : Type u_6} {Aₛ : Type u_7} [CommSemiring A] [Algebra R A] [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] : IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ

instance instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid {R : Type u_1} [CommSemiring R] (S : Submonoid R) {A : Type u_6} {Aₛ : Type u_7} [CommSemiring A] [Algebra R A] [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] [h : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] : IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap

Equations

• ⋯ = ⋯

theorem isLocalizedModule_iff_isLocalization' {R : Type u_1} [CommSemiring R] (S : Submonoid R) (R' : Type u_6) [CommSemiring R'] [Algebra R R'] : IsLocalizedModule S (Algebra.ofId R R').toLinearMap ↔ IsLocalization S R'

noncomputable def LocalizedModule.lift' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) : LocalizedModule 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 LocalizedModule S M → M''.

Equations

• LocalizedModule.lift' S g h m = m.liftOn (fun (p : M × ↥S) => ↑⋯.unit⁻¹ (g p.1)) ⋯

theorem LocalizedModule.lift'_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (m : M) (s : ↥S) : LocalizedModule.lift' S g h (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (g m)

theorem LocalizedModule.lift'_add {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (x : LocalizedModule S M) (y : LocalizedModule S M) : LocalizedModule.lift' S g h (x + y) = LocalizedModule.lift' S g h x + LocalizedModule.lift' S g h y

theorem LocalizedModule.lift'_smul {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (r : R) (m : LocalizedModule S M) : r • LocalizedModule.lift' S g h m = LocalizedModule.lift' S g h (r • m)

noncomputable def LocalizedModule.lift {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) : LocalizedModule 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 LocalizedModule S M → M''.

Equations

• LocalizedModule.lift S g h = { toFun := LocalizedModule.lift' S g h, map_add' := ⋯, map_smul' := ⋯ }

theorem LocalizedModule.lift_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (m : M) (s : ↥S) : (LocalizedModule.lift S g h) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (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 LocalizedModule.lift_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) : LocalizedModule.lift S g h ∘ₗ LocalizedModule.mkLinearMap 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 ∘ mkLinearMap = g.

theorem LocalizedModule.lift_unique {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M''] [Module R M] [Module R M''] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (l : LocalizedModule S M →ₗ[R] M'') (hl : l ∘ₗ LocalizedModule.mkLinearMap S M = g) : LocalizedModule.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 LocalizedModule S M ⟶ M'' such that l ∘ mkLinearMap = g then l = lift g

instance localizedModuleIsLocalizedModule {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] : IsLocalizedModule S (LocalizedModule.mkLinearMap S M)

Equations

• ⋯ = ⋯

noncomputable def IsLocalizedModule.fromLocalizedModule' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : LocalizedModule S M → M'

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

Equations

• IsLocalizedModule.fromLocalizedModule' S f p = p.liftOn (fun (x : M × ↥S) => ↑⋯.unit⁻¹ (f x.1)) ⋯

@[simp]

theorem IsLocalizedModule.fromLocalizedModule'_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : ↥S) : IsLocalizedModule.fromLocalizedModule' S f (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)

theorem IsLocalizedModule.fromLocalizedModule'_add {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (x : LocalizedModule S M) (y : LocalizedModule S M) : IsLocalizedModule.fromLocalizedModule' S f (x + y) = IsLocalizedModule.fromLocalizedModule' S f x + IsLocalizedModule.fromLocalizedModule' S f y

theorem IsLocalizedModule.fromLocalizedModule'_smul {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (r : R) (x : LocalizedModule S M) : r • IsLocalizedModule.fromLocalizedModule' S f x = IsLocalizedModule.fromLocalizedModule' S f (r • x)

noncomputable def IsLocalizedModule.fromLocalizedModule {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : LocalizedModule S M →ₗ[R] M'

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

Equations

• IsLocalizedModule.fromLocalizedModule S f = { toFun := IsLocalizedModule.fromLocalizedModule' S f, map_add' := ⋯, map_smul' := ⋯ }

theorem IsLocalizedModule.fromLocalizedModule_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : ↥S) : (IsLocalizedModule.fromLocalizedModule S f) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)

theorem IsLocalizedModule.fromLocalizedModule.inj {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : Function.Injective ⇑(IsLocalizedModule.fromLocalizedModule S f)

theorem IsLocalizedModule.fromLocalizedModule.surj {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : Function.Surjective ⇑(IsLocalizedModule.fromLocalizedModule S f)

theorem IsLocalizedModule.fromLocalizedModule.bij {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : Function.Bijective ⇑(IsLocalizedModule.fromLocalizedModule S f)

@[simp]

theorem IsLocalizedModule.iso_symm_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : ∀ (a : M'), (IsLocalizedModule.iso S f).symm a = (Equiv.ofBijective ⇑(IsLocalizedModule.fromLocalizedModule S f) ⋯).symm a

@[simp]

theorem IsLocalizedModule.iso_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : ∀ (a : LocalizedModule S M), (IsLocalizedModule.iso S f) a = IsLocalizedModule.fromLocalizedModule' S f a

noncomputable def IsLocalizedModule.iso {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : LocalizedModule S M ≃ₗ[R] M'

If (M', f : M ⟶ M') satisfies universal property of localized module, then M' is isomorphic to LocalizedModule S M as an R-module.

Equations

• One or more equations did not get rendered due to their size.

theorem IsLocalizedModule.iso_apply_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : ↥S) : (IsLocalizedModule.iso S f) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)

theorem IsLocalizedModule.iso_symm_apply_aux {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M') : (IsLocalizedModule.iso S f).symm m = LocalizedModule.mk ⋯.choose.1 ⋯.choose.2

theorem IsLocalizedModule.iso_symm_apply' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M') (a : M) (b : ↥S) (eq1 : b • m = f a) : (IsLocalizedModule.iso S f).symm m = LocalizedModule.mk a b

theorem IsLocalizedModule.iso_symm_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : ↑(IsLocalizedModule.iso S f).symm ∘ₗ f = LocalizedModule.mkLinearMap S M

noncomputable def IsLocalizedModule.lift {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap 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

• IsLocalizedModule.lift S f g h = LocalizedModule.lift S g h ∘ₗ ↑(IsLocalizedModule.iso S f).symm

theorem IsLocalizedModule.lift_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) : IsLocalizedModule.lift S f g h ∘ₗ f = g

@[simp]

theorem IsLocalizedModule.lift_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (x : M) : (IsLocalizedModule.lift S f g h) (f x) = g x

theorem IsLocalizedModule.lift_unique {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (l : M' →ₗ[R] M'') (hl : l ∘ₗ f = g) : IsLocalizedModule.lift S f g h = l

theorem IsLocalizedModule.is_universal {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M'') : (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → ∃! l : M' →ₗ[R] M'', l ∘ₗ 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 IsLocalizedModule.ringHom_ext {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (map_unit : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) ⦃j : M' →ₗ[R] M''⦄ ⦃k : M' →ₗ[R] M''⦄ (h : j ∘ₗ f = k ∘ₗ f) : j = k

noncomputable def IsLocalizedModule.linearEquiv {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M''] [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [IsLocalizedModule S f] [IsLocalizedModule 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

• IsLocalizedModule.linearEquiv S f g = (IsLocalizedModule.iso S f).symm.trans (IsLocalizedModule.iso S g)

theorem IsLocalizedModule.smul_injective {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (s : ↥S) : Function.Injective fun (m : M') => s • m

theorem IsLocalizedModule.smul_inj {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (s : ↥S) (m₁ : M') (m₂ : M') : s • m₁ = s • m₂ ↔ m₁ = m₂

noncomputable def IsLocalizedModule.mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : ↥S) : M'

mk' f m s is the fraction m/s with respect to the localization map f.

Equations

• IsLocalizedModule.mk' f m s = (IsLocalizedModule.fromLocalizedModule S f) (LocalizedModule.mk m s)

theorem IsLocalizedModule.mk'_smul {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (r : R) (m : M) (s : ↥S) : IsLocalizedModule.mk' f (r • m) s = r • IsLocalizedModule.mk' f m s

theorem IsLocalizedModule.mk'_add_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s₁ : ↥S) (s₂ : ↥S) : IsLocalizedModule.mk' f m₁ s₁ + IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)

@[simp]

theorem IsLocalizedModule.mk'_zero {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (s : ↥S) : IsLocalizedModule.mk' f 0 s = 0

@[simp]

theorem IsLocalizedModule.mk'_one {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) : IsLocalizedModule.mk' f m 1 = f m

@[simp]

theorem IsLocalizedModule.mk'_cancel {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : ↥S) : IsLocalizedModule.mk' f (s • m) s = f m

@[simp]

theorem IsLocalizedModule.mk'_cancel' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : ↥S) : s • IsLocalizedModule.mk' f m s = f m

@[simp]

theorem IsLocalizedModule.mk'_cancel_left {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s₁ : ↥S) (s₂ : ↥S) : IsLocalizedModule.mk' f (s₁ • m) (s₁ * s₂) = IsLocalizedModule.mk' f m s₂

@[simp]

theorem IsLocalizedModule.mk'_cancel_right {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s₁ : ↥S) (s₂ : ↥S) : IsLocalizedModule.mk' f (s₂ • m) (s₁ * s₂) = IsLocalizedModule.mk' f m s₁

theorem IsLocalizedModule.mk'_add {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s : ↥S) : IsLocalizedModule.mk' f (m₁ + m₂) s = IsLocalizedModule.mk' f m₁ s + IsLocalizedModule.mk' f m₂ s

theorem IsLocalizedModule.mk'_eq_mk'_iff {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s₁ : ↥S) (s₂ : ↥S) : IsLocalizedModule.mk' f m₁ s₁ = IsLocalizedModule.mk' f m₂ s₂ ↔ ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁

theorem IsLocalizedModule.mk'_neg {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : ↥S) : IsLocalizedModule.mk' f (-m) s = -IsLocalizedModule.mk' f m s

theorem IsLocalizedModule.mk'_sub {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s : ↥S) : IsLocalizedModule.mk' f (m₁ - m₂) s = IsLocalizedModule.mk' f m₁ s - IsLocalizedModule.mk' f m₂ s

theorem IsLocalizedModule.mk'_sub_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s₁ : ↥S) (s₂ : ↥S) : IsLocalizedModule.mk' f m₁ s₁ - IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)

theorem IsLocalizedModule.mk'_mul_mk'_of_map_mul {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [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₂) [IsLocalizedModule S f] (m₁ : M) (m₂ : M) (s₁ : ↥S) (s₂ : ↥S) : IsLocalizedModule.mk' f m₁ s₁ * IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (m₁ * m₂) (s₁ * s₂)

theorem IsLocalizedModule.mk'_mul_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_6} {M' : Type u_7} [Semiring M] [Semiring M'] [Algebra R M] [Algebra R M'] (f : M →ₐ[R] M') [IsLocalizedModule S f.toLinearMap] (m₁ : M) (m₂ : M) (s₁ : ↥S) (s₂ : ↥S) : IsLocalizedModule.mk' f.toLinearMap m₁ s₁ * IsLocalizedModule.mk' f.toLinearMap m₂ s₂ = IsLocalizedModule.mk' f.toLinearMap (m₁ * m₂) (s₁ * s₂)

theorem IsLocalizedModule.mk'_eq_iff {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] {f : M →ₗ[R] M'} [IsLocalizedModule S f] {m : M} {s : ↥S} {m' : M'} : IsLocalizedModule.mk' f m s = m' ↔ f m = s • m'

@[simp]

theorem IsLocalizedModule.mk'_eq_zero {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] {f : M →ₗ[R] M'} [IsLocalizedModule S f] {m : M} (s : ↥S) : IsLocalizedModule.mk' f m s = 0 ↔ f m = 0

theorem IsLocalizedModule.mk'_eq_zero' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {m : M} (s : ↥S) : IsLocalizedModule.mk' f m s = 0 ↔ ∃ (s' : ↥S), s' • m = 0

theorem IsLocalizedModule.mk_eq_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} [AddCommMonoid M] [Module R M] (s : ↥S) (m : M) : LocalizedModule.mk m s = IsLocalizedModule.mk' (LocalizedModule.mkLinearMap S M) m s

theorem IsLocalizedModule.mk'_smul_mk' {R : Type u_1} [CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] (A : Type u_5) [CommSemiring A] [Algebra R A] [Module A M'] [IsLocalization S A] [Module R M] [Module R M'] [IsScalarTower R A M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (x : R) (m : M) (s : ↥S) (t : ↥S) : IsLocalization.mk' A x s • IsLocalizedModule.mk' f m t = IsLocalizedModule.mk' f (x • m) (s * t)

theorem IsLocalizedModule.eq_zero_iff {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {m : M} : f m = 0 ↔ ∃ (s' : ↥S), s' • m = 0

theorem IsLocalizedModule.mk'_surjective {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : Function.Surjective (Function.uncurry (IsLocalizedModule.mk' f))

noncomputable def IsLocalizedModule.map {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] : (M →ₗ[R] N) →ₗ[R] M' →ₗ[R] N'

A linear map M →ₗ[R] N gives a map between localized modules Mₛ →ₗ[R] Nₛ.

Equations

• IsLocalizedModule.map S f g = { toFun := fun (h : M →ₗ[R] N) => IsLocalizedModule.lift S f (g ∘ₗ h) ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem IsLocalizedModule.map_comp {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) : (IsLocalizedModule.map S f g) h ∘ₗ f = g ∘ₗ h

@[simp]

theorem IsLocalizedModule.map_apply {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (x : M) : ((IsLocalizedModule.map S f g) h) (f x) = g (h x)

@[simp]

theorem IsLocalizedModule.map_mk' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (x : M) (s : ↥S) : ((IsLocalizedModule.map S f g) h) (IsLocalizedModule.mk' f x s) = IsLocalizedModule.mk' g (h x) s

@[simp]

theorem IsLocalizedModule.map_id {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] : (IsLocalizedModule.map S f f) LinearMap.id = LinearMap.id

@[simp]

theorem IsLocalizedModule.map_injective {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (h_inj : Function.Injective ⇑h) : Function.Injective ⇑((IsLocalizedModule.map S f g) h)

@[simp]

theorem IsLocalizedModule.map_surjective {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N : Type u_6} {N' : Type u_7} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (h_surj : Function.Surjective ⇑h) : Function.Surjective ⇑((IsLocalizedModule.map S f g) h)

theorem IsLocalizedModule.iso_localizedModule_eq_refl {R : Type u_1} [CommSemiring R] (S : Submonoid R) (M : Type u_2) [AddCommMonoid M] [Module R M] : IsLocalizedModule.iso S (LocalizedModule.mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

The linear map (LocalizedModule S M) → (LocalizedModule S M) from iso is the identity.

theorem IsLocalizedModule.map_LocalizedModules {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} [AddCommMonoid M₀] [Module R M₀] {M₁ : Type u_7} [AddCommMonoid M₁] [Module R M₁] (g : M₀ →ₗ[R] M₁) (m : M₀) (s : ↥S) : ((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Formula for IsLocalizedModule.map when each localized module is a LocalizedModule.

theorem IsLocalizedModule.map_iso_commute {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀'] (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_8} [AddCommMonoid M₁] [AddCommMonoid M₁'] [Module R M₁] [Module R M₁'] (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁] (g : M₀ →ₗ[R] M₁) : (IsLocalizedModule.map S f₀ f₁) g ∘ₗ ↑(IsLocalizedModule.iso S f₀) = ↑(IsLocalizedModule.iso S f₁) ∘ₗ (IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g

theorem LocalizedModule.map_exact {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} [AddCommMonoid M₀] [Module R M₀] {M₁ : Type u_7} [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_8} [AddCommMonoid M₂] [Module R M₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Function.Exact ⇑g ⇑h) : Function.Exact ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g) ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₁) (LocalizedModule.mkLinearMap S M₂)) h)

Localization of modules is an exact functor, proven here for LocalizedModule. See IsLocalizedModule.map_exact for the more general version.

theorem IsLocalizedModule.map_exact {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀'] (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_10} [AddCommMonoid M₁] [AddCommMonoid M₁'] [Module R M₁] [Module R M₁'] (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁] {M₂ : Type u_8} {M₂' : Type u_11} [AddCommMonoid M₂] [AddCommMonoid M₂'] [Module R M₂] [Module R M₂'] (f₂ : M₂ →ₗ[R] M₂') [IsLocalizedModule S f₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) (ex : Function.Exact ⇑g ⇑h) : Function.Exact ⇑((IsLocalizedModule.map S f₀ f₁) g) ⇑((IsLocalizedModule.map S f₁ f₂) h)

Localization of modules is an exact functor.

theorem IsLocalizedModule.map_comp' {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [AddCommMonoid M₀] [AddCommMonoid M₀'] [Module R M₀] [Module R M₀'] (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_11} [AddCommMonoid M₁] [AddCommMonoid M₁'] [Module R M₁] [Module R M₁'] (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁] {M₂ : Type u_8} {M₂' : Type u_10} [AddCommMonoid M₂] [AddCommMonoid M₂'] [Module R M₂] [Module R M₂'] (f₂ : M₂ →ₗ[R] M₂') [IsLocalizedModule S f₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂) : (IsLocalizedModule.map S f₀ f₂) (h ∘ₗ g) = (IsLocalizedModule.map S f₁ f₂) h ∘ₗ (IsLocalizedModule.map S f₀ f₁) g

Localization of composition is the composition of localization

theorem IsLocalizedModule.mkOfAlgebra {R : Type u_6} {S : Type u_7} {S' : Type u_8} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] (M : Submonoid R) (f : S →ₐ[R] S') (h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)) (h₂ : ∀ (y : S'), ∃ (x : S × ↥M), x.2 • y = f x.1) (h₃ : ∀ (x : S), f x = 0 → ∃ (m : ↥M), m • x = 0) : IsLocalizedModule M f.toLinearMap

theorem LocalizedModule.mem_ker_mkLinearMap_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] {S : Submonoid R} {m : M} : m ∈ LinearMap.ker (LocalizedModule.mkLinearMap S M) ↔ ∃ r ∈ S, r • m = 0

theorem LocalizedModule.subsingleton_iff_ker_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] {S : Submonoid R} : Subsingleton (LocalizedModule S M) ↔ LinearMap.ker (LocalizedModule.mkLinearMap S M) = ⊤

theorem LocalizedModule.subsingleton_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] {S : Submonoid R} : Subsingleton (LocalizedModule S M) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0