English
Let R be a commutative ring, S an R-algebra, M and N be R-modules with N the S-base change of M, and P an S-module compatible with R-actions. Then there is a natural isomorphism of S-modules between P ⊗_S N and P ⊗_R M.
Русский
Пусть R — коммутативное кольцо, S — R-алгебра, M и N — R-модули, причём N является основанием базового изменения M к S, и P — S-модуль, совместимый с действиями по R. Тогда существует естественное изоморождение S-сло между P ⊗_S N и P ⊗_R M.
LaTeX
$$$P \otimes_S N \cong_S P \otimes_R M$$$
Lean4
/-- Let `R` be a commutative ring, `S` be an `R`-algebra, `M` be an `R`-module, `P` be an `S`
module, `N` be the base change of `M` to `S`, then `P ⊗[S] N` is isomorphic to `P ⊗[R] M`
as `S`-modules. -/
noncomputable def tensorEquiv {f : M →ₗ[R] N} (hf : IsBaseChange S f) (P : Type*) [AddCommGroup P] [Module R P]
[Module S P] [IsScalarTower R S P] : P ⊗[S] N ≃ₗ[S] P ⊗[R] M :=
LinearEquiv.lTensor P hf.equiv.symm ≪≫ₗ AlgebraTensorModule.cancelBaseChange R S S P M
