Modules / vector spaces over localizations / fraction fields

This file contains some results about vector spaces over the field of fractions of a ring.

Main results

• LinearIndependent.localization: b is linear independent over a localization of R if it is linear independent over R itself
• Basis.ofIsLocalizedModule / Basis.localizationLocalization: promote an R-basis b of A to an Rₛ-basis of Aₛ, where Rₛ and Aₛ are localizations of R and A at s respectively
• LinearIndependent.iff_fractionRing: b is linear independent over R iff it is linear independent over Frac(R)

theorem span_eq_top_of_isLocalizedModule {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {v : Set M} (hv : Submodule.span R v = ⊤) : Submodule.span Rₛ (⇑f '' v) = ⊤

theorem LinearIndependent.of_isLocalizedModule {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} {v : ι → M} (hv : LinearIndependent R v) : LinearIndependent Rₛ (⇑f ∘ v)

theorem LinearIndependent.of_isLocalizedModule_of_isRegular {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} {v : ι → M} (hv : LinearIndependent R v) (h : ∀ (s : ↥S), IsRegular ↑s) : LinearIndependent R (⇑f ∘ v)

theorem LinearIndependent.localization {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} [AddCommMonoid M] [Module R M] [Module Rₛ M] [IsScalarTower R Rₛ M] {ι : Type u_5} {b : ι → M} (hli : LinearIndependent R b) : LinearIndependent Rₛ b

theorem IsLocalizedModule.linearIndependent_lift {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} {v : ι → Mₛ} (hf : LinearIndependent R v) : ∃ (w : ι → M), LinearIndependent R w

noncomputable def Module.Basis.ofIsLocalizedModule {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} (b : Basis ι R M) : Basis ι Rₛ Mₛ

If M has an R-basis, then localizing M at S has a basis over R localized at S.

Equations

• Module.Basis.ofIsLocalizedModule Rₛ S f b = Module.Basis.mk ⋯ ⋯

@[simp]

theorem Module.Basis.ofIsLocalizedModule_apply {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} (b : Basis ι R M) (i : ι) : (ofIsLocalizedModule Rₛ S f b) i = f (b i)

@[simp]

theorem Module.Basis.ofIsLocalizedModule_repr_apply {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} (b : Basis ι R M) (m : M) (i : ι) : ((ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)

theorem Module.Basis.ofIsLocalizedModule_span {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [AddCommMonoid M] [Module R M] [AddCommMonoid Mₛ] [Module R Mₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] {ι : Type u_5} (b : Basis ι R M) : Submodule.span R (Set.range ⇑(ofIsLocalizedModule Rₛ S f b)) = LinearMap.range f

theorem LinearIndependent.localization_localization {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [CommSemiring A] [Algebra R A] (Aₛ : Type u_4) [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} {v : ι → A} (hv : LinearIndependent R v) : LinearIndependent Rₛ (⇑(algebraMap A Aₛ) ∘ v)

theorem span_eq_top_localization_localization {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [CommSemiring A] [Algebra R A] (Aₛ : Type u_4) [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {v : Set A} (hv : Submodule.span R v = ⊤) : Submodule.span Rₛ (⇑(algebraMap A Aₛ) '' v) = ⊤

noncomputable def Module.Basis.localizationLocalization {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [CommSemiring A] [Algebra R A] (Aₛ : Type u_4) [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Basis ι R A) : Basis ι Rₛ Aₛ

If A has an R-basis, then localizing A at S has a basis over R localized at S.

A suitable instance for [Algebra A Aₛ] is localizationAlgebra.

Equations

• Module.Basis.localizationLocalization Rₛ S Aₛ b = Module.Basis.ofIsLocalizedModule Rₛ S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap b

@[simp]

theorem Module.Basis.localizationLocalization_apply {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [CommSemiring A] [Algebra R A] (Aₛ : Type u_4) [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Basis ι R A) (i : ι) : (localizationLocalization Rₛ S Aₛ b) i = (algebraMap A Aₛ) (b i)

@[simp]

theorem Module.Basis.localizationLocalization_repr_algebraMap {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [CommSemiring A] [Algebra R A] (Aₛ : Type u_4) [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Basis ι R A) (x : A) (i : ι) : ((localizationLocalization Rₛ S Aₛ b).repr ((algebraMap A Aₛ) x)) i = (algebraMap R Rₛ) ((b.repr x) i)

theorem Module.Basis.localizationLocalization_span {R : Type u_1} (Rₛ : Type u_2) [CommSemiring R] (S : Submonoid R) [CommSemiring Rₛ] [Algebra R Rₛ] [IsLocalization S Rₛ] {A : Type u_3} [CommSemiring A] [Algebra R A] (Aₛ : Type u_4) [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Basis ι R A) : Submodule.span R (Set.range ⇑(localizationLocalization Rₛ S Aₛ b)) = LinearMap.range (IsScalarTower.toAlgHom R A Aₛ)

theorem LinearIndependent.iff_fractionRing (R : Type u_3) (K : Type u_4) [CommRing R] [CommRing K] [Algebra R K] [IsFractionRing R K] {V : Type u_5} [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] {ι : Type u_6} {b : ι → V} : LinearIndependent R b ↔ LinearIndependent K b

def LinearMap.extendScalarsOfIsLocalization {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) : M →ₗ[A] N

An R-linear map between two S⁻¹R-modules is actually S⁻¹R-linear.

Equations

• LinearMap.extendScalarsOfIsLocalization S A f = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.restrictScalars_extendScalarsOfIsLocalization {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) : ↑R (extendScalarsOfIsLocalization S A f) = f

@[simp]

theorem LinearMap.extendScalarsOfIsLocalization_apply {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₗ[A] N) : extendScalarsOfIsLocalization S A (↑R f) = f

@[simp]

theorem LinearMap.extendScalarsOfIsLocalization_apply' {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) (x : M) : (extendScalarsOfIsLocalization S A f) x = f x

def LinearMap.extendScalarsOfIsLocalizationEquiv {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] : (M →ₗ[R] N) ≃ₗ[A] M →ₗ[A] N

The S⁻¹R-linear maps between two S⁻¹R-modules are exactly the R-linear maps.

Equations

• LinearMap.extendScalarsOfIsLocalizationEquiv S A = { toFun := LinearMap.extendScalarsOfIsLocalization S A, map_add' := ⋯, map_smul' := ⋯, invFun := ↑R, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearMap.extendScalarsOfIsLocalizationEquiv_apply {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) : (extendScalarsOfIsLocalizationEquiv S A) f = extendScalarsOfIsLocalization S A f

@[simp]

theorem LinearMap.extendScalarsOfIsLocalizationEquiv_symm_apply {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (fₗ : M →ₗ[A] N) : (extendScalarsOfIsLocalizationEquiv S A).symm fₗ = ↑R fₗ

def LinearEquiv.extendScalarsOfIsLocalization {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M ≃ₗ[R] N) : M ≃ₗ[A] N

An R-linear isomorphism between S⁻¹R-modules is actually S⁻¹R-linear.

Equations

• LinearEquiv.extendScalarsOfIsLocalization S A f = LinearEquiv.ofLinear (LinearMap.extendScalarsOfIsLocalization S A ↑f) (LinearMap.extendScalarsOfIsLocalization S A ↑f.symm) ⋯ ⋯

@[simp]

theorem LinearEquiv.extendScalarsOfIsLocalization_apply {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M ≃ₗ[R] N) (a : M) : (extendScalarsOfIsLocalization S A f) a = f a

@[simp]

theorem LinearEquiv.extendScalarsOfIsLocalization_symm_apply {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M ≃ₗ[R] N) (a : N) : (extendScalarsOfIsLocalization S A f).symm a = f.symm a

def LinearEquiv.extendScalarsOfIsLocalizationEquiv {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] : (M ≃ₗ[R] N) ≃ M ≃ₗ[A] N

The S⁻¹R-linear isomorphisms between two S⁻¹R-modules are exactly the R-linear isomorphisms.

Equations

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

@[simp]

theorem LinearEquiv.extendScalarsOfIsLocalizationEquiv_symm_apply {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (e : M ≃ₗ[A] N) : (extendScalarsOfIsLocalizationEquiv S A).symm e = restrictScalars R e

@[simp]

theorem LinearEquiv.extendScalarsOfIsLocalizationEquiv_apply {R : Type u_3} [CommSemiring R] (S : Submonoid R) (A : Type u_4) [CommSemiring A] [Algebra R A] [IsLocalization S A] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] (e : M ≃ₗ[R] N) : (extendScalarsOfIsLocalizationEquiv S A) e = extendScalarsOfIsLocalization S A e

noncomputable def IsLocalizedModule.mapExtendScalars {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_4} {N' : Type u_5} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (Rₛ : Type u_6) [CommSemiring Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [Module Rₛ N'] [IsScalarTower R Rₛ M'] [IsScalarTower R Rₛ N'] [IsLocalization S Rₛ] : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N'

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

Equations

• IsLocalizedModule.mapExtendScalars S f g Rₛ = ↑(LinearEquiv.restrictScalars R (LinearMap.extendScalarsOfIsLocalizationEquiv S Rₛ)) ∘ₗ IsLocalizedModule.map S f g

@[simp]

theorem IsLocalizedModule.mapExtendScalars_apply_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_4} {N' : Type u_5} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (Rₛ : Type u_6) [CommSemiring Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [Module Rₛ N'] [IsScalarTower R Rₛ M'] [IsScalarTower R Rₛ N'] [IsLocalization S Rₛ] (a✝ : M →ₗ[R] N) (a : M') : ((mapExtendScalars S f g Rₛ) a✝) a = ((map S f g) a✝) a

noncomputable def IsLocalizedModule.mapEquiv {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_4} {N' : Type u_5} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (Rₛ : Type u_6) [CommSemiring Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [Module Rₛ N'] [IsScalarTower R Rₛ M'] [IsScalarTower R Rₛ N'] [IsLocalization S Rₛ] (e : M ≃ₗ[R] N) : M' ≃ₗ[Rₛ] N'

An R-module isomorphism M ≃ₗ[R] N gives an Rₛ-module isomorphism Mₛ ≃ₗ[Rₛ] Nₛ.

Equations

• IsLocalizedModule.mapEquiv S f g Rₛ e = LinearEquiv.ofLinear ((IsLocalizedModule.mapExtendScalars S f g Rₛ) ↑e) ((IsLocalizedModule.mapExtendScalars S g f Rₛ) ↑e.symm) ⋯ ⋯

@[simp]

theorem IsLocalizedModule.mapEquiv_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_4} {N' : Type u_5} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (Rₛ : Type u_6) [CommSemiring Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [Module Rₛ N'] [IsScalarTower R Rₛ M'] [IsScalarTower R Rₛ N'] [IsLocalization S Rₛ] (e : M ≃ₗ[R] N) (a : M') : (mapEquiv S f g Rₛ e) a = ((map S f g) ↑e) a

@[simp]

theorem IsLocalizedModule.mapEquiv_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] {N : Type u_4} {N' : Type u_5} [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (Rₛ : Type u_6) [CommSemiring Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [Module Rₛ N'] [IsScalarTower R Rₛ M'] [IsScalarTower R Rₛ N'] [IsLocalization S Rₛ] (e : M ≃ₗ[R] N) (a : N') : (mapEquiv S f g Rₛ e).symm a = ((map S g f) ↑e.symm) a

noncomputable def LocalizedModule.map {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] : (M →ₗ[R] N) →ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N

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

Equations

• LocalizedModule.map S = IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N) (Localization S)

@[simp]

theorem LocalizedModule.map_mk {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (x : M) (y : ↥S) : ((map S) f) (mk x y) = mk (f x) y

@[simp]

theorem LocalizedModule.map_id {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] : (map S) LinearMap.id = LinearMap.id

theorem LocalizedModule.map_injective {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (l : M →ₗ[R] N) (hl : Function.Injective ⇑l) : Function.Injective ⇑((map S) l)

theorem LocalizedModule.map_surjective {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (l : M →ₗ[R] N) (hl : Function.Surjective ⇑l) : Function.Surjective ⇑((map S) l)

theorem LocalizedModule.restrictScalars_map_eq {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_5} [AddCommMonoid N] [Module R N] {M' : Type u_3} {N' : Type u_4} [AddCommMonoid M'] [AddCommMonoid N'] [Module R M'] [Module R N'] (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N') [IsLocalizedModule S g₁] [IsLocalizedModule S g₂] (l : M →ₗ[R] N) : ↑R ((map S) l) = ↑(IsLocalizedModule.iso S g₂).symm ∘ₗ (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)