isLocalizedModule_iff_isBaseChange
theorem isLocalizedModule_iff_isBaseChange :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommRing A]
[inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_3} [inst_4 : AddCommMonoid M]
[inst_5 : Module R M] {M' : Type u_4} [inst_6 : AddCommMonoid M'] [inst_7 : Module R M'] [inst_8 : Module A M']
[inst_9 : IsScalarTower R A M'] (f : M →ₗ[R] M'), IsLocalizedModule S f ↔ IsBaseChange A f
The theorem `isLocalizedModule_iff_isBaseChange` states that for any commutative semiring `R`, submonoid `S` of `R`, commutative ring `A`, where `A` is the localization of `R` at `S`, and for any `R`-modules `M` and `M'`, where `M'` is also an `A`-module and `R` scalars can be extended to `A` scalars, a given linear map `f : M →ₗ[R] M'` is a localization of modules if and only if this same map is a base change from `R` to `A`. In particular, this means there is an isomorphism between the localized module `LocalizedModule S M` and the tensor product `(Localization S) ⊗[R] M` where an element `m/s` in the localized module is mapped to `(1/s) ⊗ₜ m` in the tensor product.
More concisely: For any commutative semiring `R`, submonoid `S` of `R`, commutative ring `A` as its localization at `S`, and `R`-modules `M` and `M'` with `A` being an extension of scalars from `R` to `M'`, the linear map `f : M →ₗ[R] M'` is a localization of modules if and only if it is a base change from `R` to `A`, and accordingly, the localized module `LocalizedModule S M` is isomorphic to the tensor product `(Localization S) ⊗[R] M`.
|
IsLocalizedModule.isBaseChange
theorem IsLocalizedModule.isBaseChange :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommRing A]
[inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_3} [inst_4 : AddCommMonoid M]
[inst_5 : Module R M] {M' : Type u_4} [inst_6 : AddCommMonoid M'] [inst_7 : Module R M'] [inst_8 : Module A M']
[inst_9 : IsScalarTower R A M'] (f : M →ₗ[R] M') [inst_10 : IsLocalizedModule S f], IsBaseChange A f
This theorem, `IsLocalizedModule.isBaseChange`, states that for a given commutative semiring `R` with a submonoid `S`, a commutative ring `A` that is a localization of `R` at `S`, along with modules `M` and `M'` over `R` with `M'` also being a module over `A` (forming a scalar tower with `R`, `A` and `M'`), if a linear transformation `f` from `M` to `M'` satisfies the property of being a localized module with respect to `S`, then `f` also satisfies the property of being a base change with respect to `A`.
More concisely: If `M` is a localized `R`-module with respect to `S`, and `M'` is an `A`-module forming a scalar tower with `R`, `A`, and `M'`, then a linear transformation `f` from `M` to `M'` that is `S`-localized is also a base change with respect to `A`.
|