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ₛ] [hT : 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_3} (Rₛ : Type u_4) [CommRing R] (S : Submonoid R) [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ] {M : Type u_5} {M' : Type u_6} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [Module Rₛ M'] [IsScalarTower R Rₛ M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {ι : Type u_7} {v : ι → M} (hv : LinearIndependent R v) : LinearIndependent Rₛ (⇑f ∘ v)

theorem LinearIndependent.localization {R : Type u_3} (Rₛ : Type u_4) [CommRing R] (S : Submonoid R) [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ] {M : Type u_5} [AddCommGroup M] [Module R M] [Module Rₛ M] [IsScalarTower R Rₛ M] {ι : Type u_7} {b : ι → M} (hli : LinearIndependent R b) : LinearIndependent Rₛ b

noncomputable def Basis.ofIsLocalizedModule {R : Type u_1} (Rₛ : Type u_2) [CommRing R] (S : Submonoid R) [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [AddCommGroup M] [AddCommGroup Mₛ] [Module R M] [Module R Mₛ] [Module Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [IsLocalizedModule S f] [IsScalarTower R Rₛ Mₛ] {ι : 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

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

@[simp]

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

@[simp]

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

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

theorem LinearIndependent.localization_localization {R : Type u_1} (Rₛ : Type u_2) [CommRing R] (S : Submonoid R) [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ] {A : Type u_3} [CommRing A] [Algebra R A] (Aₛ : Type u_4) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : 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) [CommRing R] (S : Submonoid R) [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ] {A : Type u_3} [CommRing A] [Algebra R A] (Aₛ : Type u_4) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {v : Set A} (hv : Submodule.span R v = ⊤) : Submodule.span Rₛ (⇑(algebraMap A Aₛ) '' v) = ⊤

noncomputable def Basis.localizationLocalization {R : Type u_1} (Rₛ : Type u_2) [CommRing R] (S : Submonoid R) [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ] {A : Type u_3} [CommRing A] [Algebra R A] (Aₛ : Type u_4) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : 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

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

@[simp]

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

@[simp]

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

theorem Basis.localizationLocalization_span {R : Type u_1} (Rₛ : Type u_2) [CommRing R] (S : Submonoid R) [CommRing Rₛ] [Algebra R Rₛ] [hT : IsLocalization S Rₛ] {A : Type u_3} [CommRing A] [Algebra R A] (Aₛ : Type u_4) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] {ι : Type u_5} (b : Basis ι R A) : Submodule.span R (Set.range ⇑(Basis.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] [Field 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 (LinearMap.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) : LinearMap.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) : (LinearMap.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) : (LinearMap.extendScalarsOfIsLocalizationEquiv S A) f = LinearMap.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) : (LinearMap.extendScalarsOfIsLocalizationEquiv S A).symm fₗ = ↑R fₗ

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') : ((IsLocalizedModule.mapExtendScalars S f g Rₛ) a✝) a = ((IsLocalizedModule.map S f g) a✝) 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) : ((LocalizedModule.map S) f) (LocalizedModule.mk x y) = LocalizedModule.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] : (LocalizedModule.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 ⇑((LocalizedModule.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 ⇑((LocalizedModule.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 ((LocalizedModule.map S) l) = ↑(IsLocalizedModule.iso S g₂).symm ∘ₗ (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)