# 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) [] (S : ) [] [Algebra R Rₛ] [hT : ] {M : Type u_3} {M' : Type u_4} [] [Module R M] [] [Module R M'] [Module Rₛ M'] [IsScalarTower R Rₛ M'] (f : M →ₗ[R] M') [] {v : Set M} (hv : = ) :
Submodule.span Rₛ (f '' v) =
theorem LinearIndependent.of_isLocalizedModule {R : Type u_1} (Rₛ : Type u_2) [] (S : ) [] [Algebra R Rₛ] [hT : ] {M : Type u_3} {M' : Type u_4} [] [Module R M] [] [Module R M'] [Module Rₛ M'] [IsScalarTower R Rₛ M'] (f : M →ₗ[R] M') [] {ι : Type u_5} {v : ιM} (hv : ) :
LinearIndependent Rₛ (f v)
theorem LinearIndependent.localization {R : Type u_1} (Rₛ : Type u_2) [] (S : ) [] [Algebra R Rₛ] [hT : ] {M : Type u_3} [] [Module R M] [Module Rₛ M] [IsScalarTower R Rₛ M] {ι : Type u_5} {b : ιM} (hli : ) :
noncomputable def Basis.ofIsLocalizedModule {R : Type u_1} (Rₛ : Type u_2) [] (S : ) [CommRing Rₛ] [Algebra R Rₛ] [hT : ] {M : Type u_3} {Mₛ : Type u_4} [] [] [Module R M] [Module R Mₛ] [Module Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [] [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
Instances For
@[simp]
theorem Basis.ofIsLocalizedModule_apply {R : Type u_1} (Rₛ : Type u_2) [] (S : ) [CommRing Rₛ] [Algebra R Rₛ] [hT : ] {M : Type u_3} {Mₛ : Type u_4} [] [] [Module R M] [Module R Mₛ] [Module Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [] [IsScalarTower R Rₛ Mₛ] {ι : Type u_5} (b : Basis ι R M) (i : ι) :
() i = f (b i)
@[simp]
theorem Basis.ofIsLocalizedModule_repr_apply {R : Type u_1} (Rₛ : Type u_2) [] (S : ) [CommRing Rₛ] [Algebra R Rₛ] [hT : ] {M : Type u_3} {Mₛ : Type u_4} [] [] [Module R M] [Module R Mₛ] [Module Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [] [IsScalarTower R Rₛ Mₛ] {ι : Type u_5} (b : Basis ι R M) (m : M) (i : ι) :
(().repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)
theorem Basis.ofIsLocalizedModule_span {R : Type u_1} (Rₛ : Type u_2) [] (S : ) [CommRing Rₛ] [Algebra R Rₛ] [hT : ] {M : Type u_3} {Mₛ : Type u_4} [] [] [Module R M] [Module R Mₛ] [Module Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [] [IsScalarTower R Rₛ Mₛ] {ι : Type u_5} (b : Basis ι R M) :
theorem LinearIndependent.localization_localization {R : Type u_3} (Rₛ : Type u_4) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_5} [] [Algebra R A] (Aₛ : Type u_6) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : ] {ι : Type u_7} {v : ιA} (hv : ) :
LinearIndependent Rₛ ((algebraMap A Aₛ) v)
theorem span_eq_top_localization_localization {R : Type u_3} (Rₛ : Type u_4) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_5} [] [Algebra R A] (Aₛ : Type u_6) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : ] {v : Set A} (hv : = ) :
Submodule.span Rₛ ((algebraMap A Aₛ) '' v) =
noncomputable def Basis.localizationLocalization {R : Type u_3} (Rₛ : Type u_4) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_5} [] [Algebra R A] (Aₛ : Type u_6) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : ] {ι : Type u_7} (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
Instances For
@[simp]
theorem Basis.localizationLocalization_apply {R : Type u_3} (Rₛ : Type u_4) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_5} [] [Algebra R A] (Aₛ : Type u_6) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : ] {ι : Type u_7} (b : Basis ι R A) (i : ι) :
() i = (algebraMap A Aₛ) (b i)
@[simp]
theorem Basis.localizationLocalization_repr_algebraMap {R : Type u_3} (Rₛ : Type u_4) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_5} [] [Algebra R A] (Aₛ : Type u_6) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : ] {ι : Type u_7} (b : Basis ι R A) (x : A) (i : ι) :
(().repr ((algebraMap A Aₛ) x)) i = (algebraMap R Rₛ) ((b.repr x) i)
theorem Basis.localizationLocalization_span {R : Type u_3} (Rₛ : Type u_4) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_5} [] [Algebra R A] (Aₛ : Type u_6) [CommRing Aₛ] [Algebra A Aₛ] [Algebra Rₛ Aₛ] [Algebra R Aₛ] [IsScalarTower R Rₛ Aₛ] [IsScalarTower R A Aₛ] [hA : ] {ι : Type u_7} (b : Basis ι R A) :
theorem LinearIndependent.iff_fractionRing (R : Type u_3) (K : Type u_4) [] [] [Algebra R K] [] {V : Type u_5} [] [Module R V] [Module K V] [] {ι : Type u_6} {b : ιV} :
def LinearMap.extendScalarsOfIsLocalization {R : Type u_3} [] (S : ) (A : Type u_4) [] [Algebra R A] [] {M : Type u_5} {N : Type u_6} [] [Module R M] [Module A M] [] [] [Module R N] [Module A N] [] (f : M →ₗ[R] N) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearMap.restrictScalars_extendScalarsOfIsLocalization {R : Type u_3} [] (S : ) (A : Type u_4) [] [Algebra R A] [] {M : Type u_5} {N : Type u_6} [] [Module R M] [Module A M] [] [] [Module R N] [Module A N] [] (f : M →ₗ[R] N) :
R = f
@[simp]
theorem LinearMap.extendScalarsOfIsLocalization_apply {R : Type u_3} [] (S : ) (A : Type u_4) [] [Algebra R A] [] {M : Type u_5} {N : Type u_6} [] [Module R M] [Module A M] [] [] [Module R N] [Module A N] [] (f : M →ₗ[A] N) :
= f