Modules / vector spaces over localizations / fraction fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains some results about vector spaces over the field of fractions of a ring.
Main results #
linear_independent.localization:bis linear independent over a localization ofRif it is linear independent overRitselfbasis.localization_localization: promote anR-basisbofAto anRₛ-basis ofAₛ, whereRₛandAₛare localizations ofRandAatsrespectivelylinear_independent.iff_fraction_ring:bis linear independent overRiff it is linear independent overFrac(R)
theorem
linear_independent.localization
{R : Type u_1}
(Rₛ : Type u_2)
[comm_ring R]
[comm_ring Rₛ]
[algebra R Rₛ]
(S : submonoid R)
[hT : is_localization S Rₛ]
{M : Type u_3}
[add_comm_monoid M]
[module R M]
[module Rₛ M]
[is_scalar_tower R Rₛ M]
{ι : Type u_4}
{b : ι → M}
(hli : linear_independent R b) :
linear_independent Rₛ b
theorem
linear_independent.localization_localization
{R : Type u_1}
(Rₛ : Type u_2)
[comm_ring R]
[comm_ring Rₛ]
[algebra R Rₛ]
(S : submonoid R)
[hT : is_localization S Rₛ]
{A : Type u_3}
[comm_ring A]
[algebra R A]
(Aₛ : Type u_4)
[comm_ring Aₛ]
[algebra A Aₛ]
[algebra Rₛ Aₛ]
[algebra R Aₛ]
[is_scalar_tower R Rₛ Aₛ]
[is_scalar_tower R A Aₛ]
[hA : is_localization (algebra.algebra_map_submonoid A S) Aₛ]
{ι : Type u_5}
{v : ι → A}
(hv : linear_independent R v) :
linear_independent Rₛ (⇑(algebra_map A Aₛ) ∘ v)
theorem
span_eq_top.localization_localization
{R : Type u_1}
(Rₛ : Type u_2)
[comm_ring R]
[comm_ring Rₛ]
[algebra R Rₛ]
(S : submonoid R)
[hT : is_localization S Rₛ]
{A : Type u_3}
[comm_ring A]
[algebra R A]
(Aₛ : Type u_4)
[comm_ring Aₛ]
[algebra A Aₛ]
[algebra Rₛ Aₛ]
[algebra R Aₛ]
[is_scalar_tower R Rₛ Aₛ]
[is_scalar_tower R A Aₛ]
[hA : is_localization (algebra.algebra_map_submonoid A S) Aₛ]
{v : set A}
(hv : submodule.span R v = ⊤) :
submodule.span Rₛ (⇑(algebra_map A Aₛ) '' v) = ⊤
noncomputable
def
basis.localization_localization
{R : Type u_1}
(Rₛ : Type u_2)
[comm_ring R]
[comm_ring Rₛ]
[algebra R Rₛ]
(S : submonoid R)
[hT : is_localization S Rₛ]
{A : Type u_3}
[comm_ring A]
[algebra R A]
(Aₛ : Type u_4)
[comm_ring Aₛ]
[algebra A Aₛ]
[algebra Rₛ Aₛ]
[algebra R Aₛ]
[is_scalar_tower R Rₛ Aₛ]
[is_scalar_tower R A Aₛ]
[hA : is_localization (algebra.algebra_map_submonoid 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 localization_algebra.
Equations
- basis.localization_localization Rₛ S Aₛ b = basis.mk _ _
@[simp]
theorem
basis.localization_localization_apply
{R : Type u_1}
(Rₛ : Type u_2)
[comm_ring R]
[comm_ring Rₛ]
[algebra R Rₛ]
(S : submonoid R)
[hT : is_localization S Rₛ]
{A : Type u_3}
[comm_ring A]
[algebra R A]
(Aₛ : Type u_4)
[comm_ring Aₛ]
[algebra A Aₛ]
[algebra Rₛ Aₛ]
[algebra R Aₛ]
[is_scalar_tower R Rₛ Aₛ]
[is_scalar_tower R A Aₛ]
[hA : is_localization (algebra.algebra_map_submonoid A S) Aₛ]
{ι : Type u_5}
(b : basis ι R A)
(i : ι) :
⇑(basis.localization_localization Rₛ S Aₛ b) i = ⇑(algebra_map A Aₛ) (⇑b i)
@[simp]
theorem
basis.localization_localization_repr_algebra_map
{R : Type u_1}
(Rₛ : Type u_2)
[comm_ring R]
[comm_ring Rₛ]
[algebra R Rₛ]
(S : submonoid R)
[hT : is_localization S Rₛ]
{A : Type u_3}
[comm_ring A]
[algebra R A]
(Aₛ : Type u_4)
[comm_ring Aₛ]
[algebra A Aₛ]
[algebra Rₛ Aₛ]
[algebra R Aₛ]
[is_scalar_tower R Rₛ Aₛ]
[is_scalar_tower R A Aₛ]
[hA : is_localization (algebra.algebra_map_submonoid A S) Aₛ]
{ι : Type u_5}
(b : basis ι R A)
(x : A)
(i : ι) :
⇑(⇑((basis.localization_localization Rₛ S Aₛ b).repr) (⇑(algebra_map A Aₛ) x)) i = ⇑(algebra_map R Rₛ) (⇑(⇑(b.repr) x) i)
theorem
linear_independent.iff_fraction_ring
(R : Type u_1)
(K : Type u_2)
[comm_ring R]
[field K]
[algebra R K]
[is_fraction_ring R K]
{V : Type u_3}
[add_comm_group V]
[module R V]
[module K V]
[is_scalar_tower R K V]
{ι : Type u_4}
{b : ι → V} :
linear_independent R b ↔ linear_independent K b