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] [CommRing Rₛ] [Algebra R Rₛ] (S : Submonoid R) [hT : IsLocalization S Rₛ] {M : Type u_3} [AddCommMonoid M] [Module R M] [Module Rₛ M] [IsScalarTower R Rₛ M] {ι : Type u_4} {b : ι → M} (hli : LinearIndependent R b) : LinearIndependent Rₛ b

theorem LinearIndependent.localization_localization {R : Type u_1} (Rₛ : Type u_2) [CommRing R] [CommRing Rₛ] [Algebra R Rₛ] (S : Submonoid 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 SpanEqTop.localization_localization {R : Type u_1} (Rₛ : Type u_2) [CommRing R] [CommRing Rₛ] [Algebra R Rₛ] (S : Submonoid 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] [CommRing Rₛ] [Algebra R Rₛ] (S : Submonoid 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.mk (_ : LinearIndependent Rₛ (↑(algebraMap A Aₛ) ∘ ↑b)) (_ : ⊤ ≤ Submodule.span Rₛ (Set.range (↑(algebraMap A Aₛ) ∘ ↑b)))

@[simp]

theorem Basis.localizationLocalization_apply {R : Type u_1} (Rₛ : Type u_2) [CommRing R] [CommRing Rₛ] [Algebra R Rₛ] (S : Submonoid 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] [CommRing Rₛ] [Algebra R Rₛ] (S : Submonoid 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] [CommRing Rₛ] [Algebra R Rₛ] (S : Submonoid 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_1) (K : Type u_2) [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] {V : Type u_3} [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] {ι : Type u_4} {b : ι → V} : LinearIndependent R b ↔ LinearIndependent K b

def LinearMap.extendScalarsOfIsLocalization {R : Type u_1} [CommRing R] (S : Submonoid R) (A : Type u_2) [CommRing A] [Algebra R A] [IsLocalization S A] {M : Type u_3} {N : Type u_4} [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

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

@[simp]

theorem LinearMap.restrictScalars_extendScalarsOfIsLocalization {R : Type u_1} [CommRing R] (S : Submonoid R) (A : Type u_2) [CommRing A] [Algebra R A] [IsLocalization S A] {M : Type u_3} {N : Type u_4} [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_1} [CommRing R] (S : Submonoid R) (A : Type u_2) [CommRing A] [Algebra R A] [IsLocalization S A] {M : Type u_3} {N : Type u_4} [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