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:bis linear independent over a localization ofRif it is linear independent overRitselfBasis.ofIsLocalizedModule/Basis.localizationLocalization: promote anR-basisbofAto anRₛ-basis ofAₛ, whereRₛandAₛare localizations ofRandAatsrespectivelyLinearIndependent.iff_fractionRing:bis linear independent overRiff it is linear independent overFrac(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_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]
{ι : Type u_5}
{v : ι → M}
(hv : LinearIndependent R v)
:
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ₛ]
[hT : 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
noncomputable def
Basis.ofIsLocalizedModule
{R : Type u_1}
(Rₛ : Type u_2)
[CommSemiring 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 ⋯ ⋯
Instances For
@[simp]
theorem
Basis.ofIsLocalizedModule_apply
{R : Type u_1}
(Rₛ : Type u_2)
[CommSemiring 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)
[CommSemiring 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)
[CommSemiring 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)
[CommSemiring 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)
[CommSemiring 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)
[CommSemiring 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
Instances For
@[simp]
theorem
Basis.localizationLocalization_apply
{R : Type u_1}
(Rₛ : Type u_2)
[CommSemiring 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)
[CommSemiring 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)
[CommSemiring 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)
:
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' := ⋯ }
Instances For
@[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