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
:b
is linear independent over a localization ofR
if it is linear independent overR
itselfBasis.ofIsLocalizedModule
/Basis.localizationLocalization
: promote anR
-basisb
ofA
to anRₛ
-basis ofAₛ
, whereRₛ
andAₛ
are localizations ofR
andA
ats
respectivelyLinearIndependent.iff_fractionRing
:b
is linear independent overR
iff it is linear independent overFrac(R)
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
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
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
The S⁻¹R
-linear maps between two S⁻¹R
-modules are exactly the R
-linear maps.
Equations
- LinearMap.extendScalarsOfIsLocalizationEquiv S A = { toFun := LinearMap.extendScalarsOfIsLocalization S A, map_add' := ⋯, map_smul' := ⋯, invFun := ↑R, left_inv := ⋯, right_inv := ⋯ }
Instances For
An R
-linear isomorphism between S⁻¹R
-modules is actually S⁻¹R
-linear.
Equations
Instances For
The S⁻¹R
-linear isomorphisms between two S⁻¹R
-modules are exactly the R
-linear
isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A linear map M →ₗ[R] N
gives a map between localized modules Mₛ →ₗ[Rₛ] Nₛ
.
Equations
Instances For
An R
-module isomorphism M ≃ₗ[R] N
gives an Rₛ
-module isomorphism Mₛ ≃ₗ[Rₛ] Nₛ
.
Equations
- IsLocalizedModule.mapEquiv S f g Rₛ e = LinearEquiv.ofLinear ((IsLocalizedModule.mapExtendScalars S f g Rₛ) ↑e) ((IsLocalizedModule.mapExtendScalars S g f Rₛ) ↑e.symm) ⋯ ⋯
Instances For
A linear map M →ₗ[R] N
gives a map between localized modules Mₛ →ₗ[Rₛ] Nₛ
.