# Documentation

Mathlib.RingTheory.Localization.Module

# 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.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 LinearIndependent.localization {R : Type u_1} (Rₛ : Type u_2) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {M : Type u_3} [] [Module R M] [Module Rₛ M] [IsScalarTower R Rₛ M] {ι : Type u_4} {b : ιM} (hli : ) :
theorem LinearIndependent.localization_localization {R : Type u_1} (Rₛ : Type u_2) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_3} [] [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 : ] {ι : Type u_5} {v : ιA} (hv : ) :
LinearIndependent Rₛ (↑(algebraMap A Aₛ) v)
theorem SpanEqTop.localization_localization {R : Type u_1} (Rₛ : Type u_2) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_3} [] [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 : ] {v : Set A} (hv : = ) :
Submodule.span Rₛ (↑(algebraMap A Aₛ) '' v) =
noncomputable def Basis.localizationLocalization {R : Type u_1} (Rₛ : Type u_2) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_3} [] [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 : ] {ι : 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.

Instances For
@[simp]
theorem Basis.localizationLocalization_apply {R : Type u_1} (Rₛ : Type u_2) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_3} [] [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 : ] {ι : Type u_5} (b : Basis ι R A) (i : ι) :
↑() i = ↑(algebraMap A Aₛ) (b i)
@[simp]
theorem Basis.localizationLocalization_repr_algebraMap {R : Type u_1} (Rₛ : Type u_2) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_3} [] [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 : ] {ι : Type u_5} (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_1} (Rₛ : Type u_2) [] [CommRing Rₛ] [Algebra R Rₛ] (S : ) [hT : ] {A : Type u_3} [] [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 : ] {ι : Type u_5} (b : Basis ι R A) :
theorem LinearIndependent.iff_fractionRing (R : Type u_1) (K : Type u_2) [] [] [Algebra R K] [] {V : Type u_3} [] [Module R V] [Module K V] [] {ι : Type u_4} {b : ιV} :
def LinearMap.extendScalarsOfIsLocalization {R : Type u_1} [] (S : ) (A : Type u_2) [] [Algebra R A] [] {M : Type u_3} {N : Type u_4} [] [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.

Instances For
@[simp]
theorem LinearMap.restrictScalars_extendScalarsOfIsLocalization {R : Type u_1} [] (S : ) (A : Type u_2) [] [Algebra R A] [] {M : Type u_3} {N : Type u_4} [] [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_1} [] (S : ) (A : Type u_2) [] [Algebra R A] [] {M : Type u_3} {N : Type u_4} [] [Module R M] [Module A M] [] [] [Module R N] [Module A N] [] (f : M →ₗ[A] N) :
= f