# 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`.

source
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

Equations

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

Instances For

source
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)
source
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 := ⋯ }

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

Instances For

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

Instances For

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

Instances For

source
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)
source
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 → α`.

Equations

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

Instances For

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

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

source
@[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
source
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)) ⋯ }

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

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

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

source
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) ⋯ }

source
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

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

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

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

source
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

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

source
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 = { toSemiring := have this := inferInstance; this, mul_comm := ⋯ }

source
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

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

source
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 = { toRing := have this := inferInstance; this, mul_comm := ⋯ }

source
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₂)
source
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.

source
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)
source
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')
source
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)
source
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 = { toSMul := LocalizedModule.instSMul T, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source
@[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
source
@[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
source
@[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
source
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.compHom (LocalizedModule S M) (algebraMap R (Localization S))

source
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
source
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
source
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
source
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₂)
source
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₂)
source
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 ⋯ ⋯

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

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

Equations

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

Instances For

source
@[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
source
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)`.

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

Instances For

source
@[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)) ⋯
source
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
source
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
source
class IsLocalizedModule {R : Type u_1} [CommSemiring R] {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (S : Submonoid R) (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₂

Instances

source
theorem isLocalizedModule_iff {R : Type u_1} [CommSemiring R] {M : Type u_2} {M' : Type u_3} [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R M'] (S : Submonoid R) (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₂
source
@[deprecated IsLocalizedModule.surj (since := "2025-09-05")]
theorem IsLocalizedModule.surj' {R : Type u_1} {inst✝ : CommSemiring R} {M : Type u_2} {M' : Type u_3} {inst✝¹ : AddCommMonoid M} {inst✝² : AddCommMonoid M'} {inst✝³ : Module R M} {inst✝⁴ : Module R M'} (S : Submonoid R) (f : M →ₗ[R] M') [self : IsLocalizedModule S f] (y : M') :
∃ (x : M × ↥S), x.2 • y = f x.1

Alias of `IsLocalizedModule.surj`.

source
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₂
source
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
source
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)
source
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)
source
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
source
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)) ⋯

Instances For

source
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)
source
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
source
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)
source
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' := ⋯ }

Instances For

source
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`.

source
@[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
source
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`.

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

source
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)
source
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
source
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
source
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)) ⋯

Instances For

source
@[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)
source
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
source
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)
source
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' := ⋯ }

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

source
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
source
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₂)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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₂
source
@[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₁
source
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
source
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₁
source
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
source
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
source
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₂)
source
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₂)
source
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₂)
source
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'
source
@[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
source
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
source
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
source
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)
source
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
source
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))
source
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`).

Equations

- IsLocalizedModule.liftOfLE S₁ S₂ h f₁ f₂ = IsLocalizedModule.lift S₁ f₁ f₂ ⋯

Instances For

source
@[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`).

Equations

- LocalizedModule.liftOfLE S₁ S₂ h = IsLocalizedModule.liftOfLE S₁ S₂ h (LocalizedModule.mkLinearMap S₁ M) (LocalizedModule.mkLinearMap S₂ M)

Instances For

source
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₂
source
@[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
source
@[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`.

source
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₂)
source
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
source
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
source
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' := ⋯ }

Instances For

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

source
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`.

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

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

Equations

- IsLocalizedModule.module S f = AddEquiv.module A (IsLocalizedModule.iso S f).symm.toAddEquiv

Instances For

source
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'
source
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
source
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 = ⊤
source
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
source
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
source
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) = ⊤
source
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
source
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)
source
theorem IsLocalizedModule.noZeroSMulDivisors {R : Type u_1} {M : Type u_2} {A : Type u_3} {N : Type u_4} [CommRing R] [AddCommMonoid M] [Module R M] [CommRing A] [AddCommMonoid N] [Module A N] [Algebra R A] [Module R N] [IsScalarTower R A N] (f : M →ₗ[R] N) (S : Submonoid R) [NoZeroSMulDivisors R M] [IsLocalization S A] [IsLocalizedModule S f] :
NoZeroSMulDivisors A N
source
instance IsLocalizedModule.instNoZeroSMulDivisorsLocalizationLocalizedModule {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (S : Submonoid R) [NoZeroSMulDivisors R M] :
NoZeroSMulDivisors (Localization S) (LocalizedModule S M)