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 := (_ : Equivalence (LocalizedModule.r S M)) }

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

• LocalizedModule.liftOn x 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.liftOn (LocalizedModule.mk m s) 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

• LocalizedModule.liftOn₂ x 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.liftOn₂ (LocalizedModule.mk m s) (LocalizedModule.mk m' s') f wd = f (m, s) (m', s')

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

Equations

• LocalizedModule.instZeroLocalizedModule = { 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.instAddLocalizedModule {R : Type u} [CommSemiring R] {S : Submonoid R} {M : Type v} [AddCommMonoid M] [Module R M] : Add (LocalizedModule S M)

Equations

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

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

Equations

• LocalizedModule.instAddCommMonoidLocalizedModule = AddCommMonoid.mk (_ : ∀ (x y : LocalizedModule S M), x + y = y + x)

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

Equations

• LocalizedModule.instAddCommGroupLocalizedModuleToAddCommMonoid = let src := let_fun this := inferInstance; this; AddCommGroup.mk (_ : ∀ (a b : LocalizedModule S M), a + b = b + a)

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.instMonoidLocalizedModuleToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModule {R : Type u} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {S : Submonoid R} : Monoid (LocalizedModule S A)

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.instSMulLocalizedModule {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 (_ : ∀ (x y : T) (p : LocalizedModule S M), (x + y) • p = x • p + y • p) (_ : ∀ (p : LocalizedModule S M), 0 • p = 0)

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

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

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'_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.instAlgebraLocalizedModuleToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleInstSemiringLocalizedModuleToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModule {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

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

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

• (_ : IsScalarTower R T (LocalizedModule S M)) = (_ : 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)

Equations

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

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

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

@[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 = LocalizedModule.liftOn p (fun (p : M × ↥S) => LocalizedModule.mk p.1 (p.2 * s)) (_ : ∀ (x x_1 : M × ↥S), x ≈ x_1 → (fun (p : M × ↥S) => LocalizedModule.mk p.1 (p.2 * s)) x = (fun (p : M × ↥S) => LocalizedModule.mk p.1 (p.2 * s)) x_1)

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

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

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.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 (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ)) ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ

instance instIsLocalizedModuleToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModuleToModuleToLinearMapToAlgHom {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 (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ))

Equations

• (_ : IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ))) = (_ : IsLocalizedModule S (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₛ)))

theorem isLocalizedModule_iff_isLocalization' {R : Type u_1} [CommSemiring R] (S : Submonoid R) (R' : Type u_6) [CommSemiring R'] [Algebra R R'] : IsLocalizedModule S (AlgHom.toLinearMap (Algebra.ofId R R')) ↔ 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

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

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) = ↑(IsUnit.unit (_ : IsUnit ((algebraMap R (Module.End R M'')) ↑s)))⁻¹ (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

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

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) = ↑(IsUnit.unit (_ : IsUnit ((algebraMap R (Module.End R M'')) ↑s)))⁻¹ (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

• (_ : IsLocalizedModule S (LocalizedModule.mkLinearMap S M)) = (_ : IsLocalizedModule S (LocalizedModule.mkLinearMap S M))

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

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

@[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) = ↑(IsUnit.unit (_ : IsUnit ((algebraMap R (Module.End R M')) ↑s)))⁻¹ (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

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

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) = ↑(IsUnit.unit (_ : IsUnit ((algebraMap R (Module.End R M')) ↑s)))⁻¹ (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_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

@[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'), (LinearEquiv.symm (IsLocalizedModule.iso S f)) a = (Equiv.ofBijective ⇑(IsLocalizedModule.fromLocalizedModule S f) (_ : Function.Bijective ⇑(IsLocalizedModule.fromLocalizedModule S f))).symm 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) = ↑(IsUnit.unit (_ : IsUnit ((algebraMap R (Module.End R M')) ↑s)))⁻¹ (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') : (LinearEquiv.symm (IsLocalizedModule.iso S f)) m = LocalizedModule.mk (Exists.choose (_ : ∃ (x : M × ↥S), x.2 • m = f x.1)).1 (Exists.choose (_ : ∃ (x : M × ↥S), x.2 • m = f x.1)).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) : (LinearEquiv.symm (IsLocalizedModule.iso S f)) 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] : ↑(LinearEquiv.symm (IsLocalizedModule.iso S f)) ∘ₗ 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 = LinearMap.comp (LocalizedModule.lift S g h) ↑(LinearEquiv.symm (IsLocalizedModule.iso S f))

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

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 = LinearEquiv.trans (LinearEquiv.symm (IsLocalizedModule.iso S f)) (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 (AlgHom.toLinearMap f)] (m₁ : M) (m₂ : M) (s₁ : ↥S) (s₂ : ↥S) : IsLocalizedModule.mk' (AlgHom.toLinearMap f) m₁ s₁ * IsLocalizedModule.mk' (AlgHom.toLinearMap f) m₂ s₂ = IsLocalizedModule.mk' (AlgHom.toLinearMap f) (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'

Porting note: simp can prove this @[simp]

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

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 (AlgHom.toLinearMap f)