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 #

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) :
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
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) :
    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
    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) :
      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} :
      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
      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) :
        @[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) :
        @[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) :