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

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) (LocalizedModule.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' : M} {s : ↥S} {s' : ↥S} :

LocalizedModule.mk m s = LocalizedModule.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), β (LocalizedModule.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), β (LocalizedModule.mk m s) (LocalizedModule.mk m' s')) (x : LocalizedModule S M) (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) :

(LocalizedModule.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 : LocalizedModule S M) (y : LocalizedModule S M) (f : M × ↥S → M × ↥S → α) (wd : ∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q') :

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

Equations

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

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' : M) (s : ↥S) (s' : ↥S) :

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

LocalizedModule.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 : M} {m2 : M} {s1 : ↥S} {s2 : ↥S} :

LocalizedModule.mk m1 s1 + LocalizedModule.mk m2 s2 = LocalizedModule.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

LocalizedModule.instAddCommMonoid = AddCommMonoid.mk ⋯

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

LocalizedModule.instAddCommGroup = let __src := let_fun this := inferInstance; this; AddCommGroup.mk ⋯

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

LocalizedModule.mk (-m) s = -LocalizedModule.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

LocalizedModule.instMonoid = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

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

LocalizedModule.instSemiring = let __src := let_fun this := inferInstance; this; let __src_1 := let_fun this := inferInstance; this; Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

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 = let __src := let_fun this := inferInstance; this; CommSemiring.mk ⋯

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 = let __src := let_fun this := inferInstance; this; CommRing.mk ⋯

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₂ : A} {s₁ : ↥S} {s₂ : ↥S} :

LocalizedModule.mk a₁ s₁ * LocalizedModule.mk a₂ s₂ = LocalizedModule.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 • LocalizedModule.mk m s = LocalizedModule.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' : ↥S) :

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

Localization.mk r s • LocalizedModule.mk m t = LocalizedModule.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 = Module.mk ⋯ ⋯

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 : ↥S) (m : M) :

LocalizedModule.mk (s' • m) (s' * s) = LocalizedModule.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) :

LocalizedModule.mk (s • m) s = LocalizedModule.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' : ↥S) (m : M) :

LocalizedModule.mk (s' • m) (s * s') = LocalizedModule.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' = let __src := Module.compHom (LocalizedModule S M) (algebraMap R (Localization S)); Module.mk ⋯ ⋯

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

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₁ : LocalizedModule S A) (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₁ : LocalizedModule S A) (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) = LocalizedModule.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) = LocalizedModule.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)

Equations

⋯ = ⋯

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

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

source

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

(LocalizedModule.divBy s) p = p.liftOn (fun (p : M × ↥S) => LocalizedModule.mk p.1 (p.2 * s)) ⋯

source

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

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

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

source

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₂

source

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₂

Instances

source

theorem IsLocalizedModule.map_units {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') [self : IsLocalizedModule S f] (x : ↥S) :

IsUnit ((algebraMap R (Module.End R M')) ↑x)

source

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'} [self : IsLocalizedModule S f] (y : M') :

∃ (x : M × ↥S), x.2 • y = f x.1

source

theorem IsLocalizedModule.exists_of_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'} [self : IsLocalizedModule S f] {x₁ : M} {x₂ : M} :

f x₁ = f x₂ → ∃ (c : ↥S), c • x₁ = c • x₂

source

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

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₁ : M} {x₂ : M} :

f x₁ = f x₂ ↔ ∃ (c : ↥S), c • x₁ = c • x₂

source

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)

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

theorem isLocalizedModule_iff_isLocalization {R : Type u_1} [CommSemiring R] {S : Submonoid R} {A : Type u_6} {Aₛ : Type u_7} [CommSemiring A] [Algebra R A] [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] :

IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ

source

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

IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap

Equations

⋯ = ⋯

source

theorem isLocalizedModule_iff_isLocalization' {R : Type u_1} [CommSemiring R] (S : Submonoid R) (R' : Type u_6) [CommSemiring R'] [Algebra R R'] :

IsLocalizedModule S (Algebra.ofId R R').toLinearMap ↔ IsLocalization S R'

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

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

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

(LocalizedModule.lift S g h) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (g m)

If g is a linear map M → M'' such that all scalar multiplication by s : S is invertible, then lift g m s = s⁻¹ • g m.

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

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.

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

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)

Equations

⋯ = ⋯

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

IsLocalizedModule.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 : LocalizedModule S M) (y : LocalizedModule S M) :

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

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

source

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

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

∀ (a : M'), (IsLocalizedModule.iso S f).symm a = (Equiv.ofBijective ⇑(IsLocalizedModule.fromLocalizedModule S f) ⋯).symm a

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

(IsLocalizedModule.iso S f) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)

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

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

(IsLocalizedModule.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] :

↑(IsLocalizedModule.iso S f).symm ∘ₗ f = LocalizedModule.mkLinearMap S M

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

IsLocalizedModule.lift S f g h ∘ₗ f = g

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

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

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

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

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₂ : M') :

s • m₁ = s • m₂ ↔ m₁ = m₂

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

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

IsLocalizedModule.mk' f (r • m) s = r • IsLocalizedModule.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₂ : M) (s₁ : ↥S) (s₂ : ↥S) :

IsLocalizedModule.mk' f m₁ s₁ + IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.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) :

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

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

IsLocalizedModule.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 • IsLocalizedModule.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₂ : ↥S) :

IsLocalizedModule.mk' f (s₁ • m) (s₁ * s₂) = IsLocalizedModule.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₂ : ↥S) :

IsLocalizedModule.mk' f (s₂ • m) (s₁ * s₂) = IsLocalizedModule.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₂ : M) (s : ↥S) :

IsLocalizedModule.mk' f (m₁ + m₂) s = IsLocalizedModule.mk' f m₁ s + IsLocalizedModule.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₂ : M) (s₁ : ↥S) (s₂ : ↥S) :

IsLocalizedModule.mk' f m₁ s₁ = IsLocalizedModule.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] [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

source

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

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] [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₂)

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} [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₂)

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₂ : M) (s₁ : ↥S) (s₂ : ↥S) :

IsLocalizedModule.mk' f.toLinearMap m₁ s₁ * IsLocalizedModule.mk' f.toLinearMap m₂ s₂ = IsLocalizedModule.mk' f.toLinearMap (m₁ * m₂) (s₁ * s₂)

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

IsLocalizedModule.mk' f m s = m' ↔ f m = s • m'

Porting note (#10618): simp can prove this @[simp]

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

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

IsLocalizedModule.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 = IsLocalizedModule.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 : ↥S) (t : ↥S) :

IsLocalization.mk' A x s • IsLocalizedModule.mk' f m t = IsLocalizedModule.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 (IsLocalizedModule.mk' f))

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} [AddCommGroup N] [AddCommGroup 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} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) :

(IsLocalizedModule.map S f g) h ∘ₗ f = g ∘ₗ h

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} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (x : M) :

((IsLocalizedModule.map S f g) h) (f x) = g (h x)

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} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (h : M →ₗ[R] N) (x : M) (s : ↥S) :

((IsLocalizedModule.map S f g) h) (IsLocalizedModule.mk' f x s) = IsLocalizedModule.mk' g (h x) s

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

IsLocalizedModule.iso S (LocalizedModule.mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

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

source

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

((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

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

source

theorem IsLocalizedModule.map_iso_commute {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M₀ : Type u_6} {M₀' : Type u_9} [AddCommGroup M₀] [AddCommGroup M₀'] [Module R M₀] [Module R M₀'] (f₀ : M₀ →ₗ[R] M₀') [IsLocalizedModule S f₀] {M₁ : Type u_7} {M₁' : Type u_8} [AddCommGroup M₁] [AddCommGroup M₁'] [Module R M₁] [Module R M₁'] (f₁ : M₁ →ₗ[R] M₁') [IsLocalizedModule S f₁] (g : M₀ →ₗ[R] M₁) :

(IsLocalizedModule.map S f₀ f₁) g ∘ₗ ↑(IsLocalizedModule.iso S f₀) = ↑(IsLocalizedModule.iso S f₁) ∘ₗ (IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g

source

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

Function.Exact ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g) ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₁) (LocalizedModule.mkLinearMap S M₂)) h)

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

source

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

Function.Exact ⇑((IsLocalizedModule.map S f₀ f₁) g) ⇑((IsLocalizedModule.map S f₁ f₂) h)

Localization of modules is an exact functor.

source

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

IsLocalizedModule M f.toLinearMap

source

theorem LocalizedModule.mem_ker_mkLinearMap_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {S : Submonoid R} {m : M} :

m ∈ LinearMap.ker (LocalizedModule.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] [AddCommGroup M] [Module R M] {S : Submonoid R} :

Subsingleton (LocalizedModule S M) ↔ LinearMap.ker (LocalizedModule.mkLinearMap S M) = ⊤

source

theorem LocalizedModule.subsingleton_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {S : Submonoid R} :

Subsingleton (LocalizedModule S M) ↔ ∀ (m : M), ∃ r ∈ S, r • m = 0

Documentation

Mathlib.Algebra.Module.LocalizedModule

Localized Module #

Main definitions #

Future work #