mathlib documentation

ring_theory.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 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) :
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) (hS : algebra.algebra_map_submonoid A S non_zero_divisors A) :
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 = ) :
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) (hS : algebra.algebra_map_submonoid A S non_zero_divisors 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
@[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) (hS : algebra.algebra_map_submonoid A S non_zero_divisors A) (i : ι) :
(basis.localization_localization Rₛ S Aₛ b hS) 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) (hS : algebra.algebra_map_submonoid A S non_zero_divisors A) (x : A) (i : ι) :
(((basis.localization_localization Rₛ S Aₛ b hS).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} :