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

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

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.

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

theorem LocalizedModule.mk_eq {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {m m' : M} {s s' : ↥S} : mk m s = 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), β (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), β (mk m s) (mk m' s')) (x 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 → α.

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) : (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 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 → α.

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) (s s' : ↥S) : (mk m s).liftOn₂ (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)

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

theorem LocalizedModule.mk_add_mk {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] {m1 m2 : M} {s1 s2 : ↥S} : mk m1 s1 + mk m2 s2 = 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)

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

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

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

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} : mk (-m) s = -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)

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

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

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

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

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} {s₁ s₂ : ↥S} : mk a₁ s₁ * mk a₂ s₂ = 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)

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 • mk m s = 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) : IsLocalization.mk' T r s • mk m s' = 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 t : ↥S) : Localization.mk r s • mk m t = 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)

@[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) (m : M) : mk (s' • m) (s' * s) = 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) : mk (s • m) s = 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) (m : M) : mk (s' • m) (s * s') = 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)

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 • mk m s = 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 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₁ 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₁ 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)

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

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)

noncomputable 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.

@[simp]

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

noncomputable 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).

@[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) : (divBy s) p = p.liftOn (fun (p : M × ↥S) => mk p.1 (p.2 * s)) ⋯

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) : (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) ((divBy s) p) = p

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_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₂

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₁ x₂ : M} : f x₁ = f x₂ ↔ ∃ (c : ↥S), c • x₁ = c • x₂

theorem IsLocalizedModule.injective_iff_isRegular {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 ⇑f ↔ ∀ (c : ↥S), IsSMulRegular M c

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

instance IsLocalizedModule.of_linearEquiv_right {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 (f ∘ₗ ↑e)

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

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

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) : lift' S g h (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 y : LocalizedModule S M) : lift' S g h (x + y) = lift' S g h x + 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 • lift' S g h m = 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''.

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) : (lift S g h) (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.

@[simp]

theorem LocalizedModule.lift_mk_one {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) : (lift S g h) (mk m 1) = 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)) : lift S g h ∘ₗ 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 ∘ₗ mkLinearMap S M = g) : 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)

theorem IsLocalizedModule.of_restrictScalars {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] {A : Type u_5} [CommSemiring A] [Algebra R A] [Module R M] (S : Submonoid R) {N : Type u_6} [AddCommMonoid N] [Module R N] [Module A M] [Module A N] [IsScalarTower R A M] [IsScalarTower R A N] (f : M →ₗ[A] N) [IsLocalizedModule S (↑R f)] : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f

theorem IsLocalizedModule.of_exists_mul_mem {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_6} [AddCommMonoid N] [Module R N] (S T : Submonoid R) (h : S ≤ T) (h' : ∀ (x : ↥T), ∃ (m : R), m * ↑x ∈ S) (f : M →ₗ[R] N) [IsLocalizedModule S f] : IsLocalizedModule T f

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

@[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) : 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 y : LocalizedModule S M) : fromLocalizedModule' S f (x + y) = fromLocalizedModule' S f x + 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 • fromLocalizedModule' S f x = 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'.

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) : (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 ⇑(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 ⇑(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 ⇑(fromLocalizedModule S f)

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.

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) : (iso S f) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)

@[simp]

theorem IsLocalizedModule.iso_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] (x : M) : (iso S f) (LocalizedModule.mk x 1) = f x

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') : (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) : (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] : ↑(iso S f).symm ∘ₗ f = LocalizedModule.mkLinearMap S M

@[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] (x : M) : (iso S f).symm (f x) = LocalizedModule.mk x 1

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

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)) : lift S f g h ∘ₗ f = g

@[simp]

theorem IsLocalizedModule.lift_iso {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] (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (x : LocalizedModule S M) : (lift S f g h) ((iso S f) x) = (LocalizedModule.lift S g h) x

@[simp]

theorem IsLocalizedModule.lift_comp_iso {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] (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) : lift S f g h ∘ₗ ↑(iso S f) = LocalizedModule.lift S g h

@[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) : (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) : 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.linearMap_ext {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] [Module R N] [AddCommMonoid N'] [Module R N'] (f' : N →ₗ[R] N') [IsLocalizedModule S f'] ⦃g g' : M' →ₗ[R] N'⦄ (h : g ∘ₗ f = g' ∘ₗ f) : g = g'

theorem IsLocalizedModule.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 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

@[simp]

theorem IsLocalizedModule.linearEquiv_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') (g : M →ₗ[R] M'') [IsLocalizedModule S f] [IsLocalizedModule S g] (x : M) : (linearEquiv S f g) (f x) = g x

@[simp]

theorem IsLocalizedModule.linearEquiv_symm_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') (g : M →ₗ[R] M'') [IsLocalizedModule S f] [IsLocalizedModule S g] (x : M) : (linearEquiv S f g).symm (g x) = f x

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') : s • m₁ = s • m₂ ↔ m₁ = m₂

theorem IsLocalizedModule.isRegular_of_smul_left_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] {m : M'} (inj : Function.Injective fun (r : R) => r • m) (s : ↥S) : IsRegular ↑s

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.

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) : mk' f (r • m) s = r • 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) (s₁ s₂ : ↥S) : mk' f m₁ s₁ + mk' f m₂ s₂ = 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) : 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) : 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) : 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 • 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) : mk' f (s₁ • m) (s₁ * s₂) = 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) : mk' f (s₂ • m) (s₁ * s₂) = 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) (s : ↥S) : mk' f (m₁ + m₂) s = mk' f m₁ s + 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) (s₁ s₂ : ↥S) : mk' f m₁ s₁ = 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] [SubtractionCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : ↥S) : mk' f (-m) s = -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] [SubtractionCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ m₂ : M) (s : ↥S) : mk' f (m₁ - m₂) s = mk' f m₁ s - 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] [SubtractionCommMonoid M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : ↥S) : mk' f m₁ s₁ - mk' f m₂ s₂ = 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} [NonUnitalNonAssocSemiring 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) (s₁ s₂ : ↥S) : mk' f m₁ s₁ * mk' f m₂ s₂ = 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) (s₁ s₂ : ↥S) : mk' f.toLinearMap m₁ s₁ * mk' f.toLinearMap m₂ s₂ = 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'} : 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) : 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) : 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 = 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 t : ↥S) : IsLocalization.mk' A x s • mk' f m t = 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 (mk' f))

noncomputable def IsLocalizedModule.liftOfLE {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M₁ : Type u_6} {M₂ : Type u_7} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [IsLocalizedModule S₁ f₁] [IsLocalizedModule S₂ f₂] : M₁ →ₗ[R] M₂

The natural map Mₛ →ₗ[R] Mₜ if s ≤ t (in Submonoid R).

@[reducible, inline]

noncomputable abbrev LocalizedModule.liftOfLE {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) : LocalizedModule S₁ M →ₗ[R] LocalizedModule S₂ M

The natural map Mₛ →ₗ[R] Mₜ if s ≤ t (in Submonoid R).

theorem IsLocalizedModule.liftOfLE_comp {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M₁ : Type u_7} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [IsLocalizedModule S₁ f₁] [IsLocalizedModule S₂ f₂] : liftOfLE S₁ S₂ h f₁ f₂ ∘ₗ f₁ = f₂

@[simp]

theorem IsLocalizedModule.liftOfLE_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M₁ : Type u_7} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [IsLocalizedModule S₁ f₁] [IsLocalizedModule S₂ f₂] (x : M) : (liftOfLE S₁ S₂ h f₁ f₂) (f₁ x) = f₂ x

@[simp]

theorem IsLocalizedModule.liftOfLE_mk' {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M₁ : Type u_7} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [IsLocalizedModule S₁ f₁] [IsLocalizedModule S₂ f₂] (m : M) (s : ↥S₁) : (liftOfLE S₁ S₂ h f₁ f₂) (mk' f₁ m s) = mk' f₂ m ⟨↑s, ⋯⟩

The image of m/s under liftOfLE is m/s.

instance IsLocalizedModule.instLiftOfLE {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M₁ : Type u_6} {M₂ : Type u_7} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (S₁ S₂ : Submonoid R) (h : S₁ ≤ S₂) (f₁ : M →ₗ[R] M₁) (f₂ : M →ₗ[R] M₂) [IsLocalizedModule S₁ f₁] [IsLocalizedModule S₂ f₂] : IsLocalizedModule S₂ (liftOfLE S₁ S₂ h f₁ f₂)

theorem IsLocalizedModule.injective_of_map_eq {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} [AddCommMonoid N] [Module R N] {g : M' →ₗ[R] N} (H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y) : Function.Injective ⇑g

theorem IsLocalizedModule.injective_of_map_zero {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_6} {M' : Type u_7} {N : Type u_8} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [AddCommGroup N] [Module R N] {g : M' →ₗ[R] N} (H : ∀ (m : M), g (f m) = 0 → f m = 0) : Function.Injective ⇑g

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ₛ.

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) : (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) : ((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) : ((map S f g) h) (mk' f x s) = 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] : (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 ⇑((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 ⇑((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] : 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) : ((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₁) : (map S f₀ f₁) g ∘ₗ ↑(iso S f₀) = ↑(iso S f₁) ∘ₗ (map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g

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₂) : (map S f₀ f₂) (h ∘ₗ g) = (map S f₁ f₂) h ∘ₗ (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} [CommSemiring R] [Ring S] [Ring 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

@[reducible]

noncomputable def IsLocalizedModule.module {R : Type u_6} {A : Type u_7} {M : Type u_8} {M' : Type u_9} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Submonoid R) [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [IsLocalization S A] (f : M →ₗ[R] M') [IsLocalizedModule S f] : Module A M'

If M' is the localization of M at S and A = S⁻¹R, then M' is an A`-module.

theorem IsLocalizedModule.isScalarTower_module {R : Type u_6} {A : Type u_7} {M : Type u_8} {M' : Type u_9} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Submonoid R) [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] [IsLocalization S A] (f : M →ₗ[R] M') [IsLocalizedModule S f] : IsScalarTower R A M'

theorem IsLocalizedModule.mem_ker_iff {R : Type u_6} {M : Type u_8} {M' : Type u_9} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (S : Submonoid R) {g : M →ₗ[R] M'} [IsLocalizedModule S g] {m : M} : m ∈ LinearMap.ker g ↔ ∃ r ∈ S, r • m = 0

theorem IsLocalizedModule.subsingleton_iff_ker_eq_top {R : Type u_6} {M : Type u_8} {M' : Type u_9} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g] : Subsingleton M' ↔ LinearMap.ker g = ⊤

theorem IsLocalizedModule.subsingleton_iff {R : Type u_6} {M : Type u_8} {M' : Type u_9} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g] : Subsingleton M' ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0

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 (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 (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

instance LocalizedModule.instSubsingleton {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] [Subsingleton M] (S : Submonoid R) : Subsingleton (LocalizedModule S M)