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) :
noncomputable def basis.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_group M] [module R M] [module Rₛ M] [is_scalar_tower R Rₛ M] {ι : Type u_4} (b : basis ι R M) :
basis ι Rₛ M

Promote a basis for M over R to a basis for M over the localization Rₛ

Equations
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} :