English
There is a natural linear equivalence S ⊗_R M modulo I-quotients with the quotient of S ⊗_R M by the image of I.
Русский
Существует естественное линейное эквивалентное отображение S ⊗_R M по отношению к модулю I с фактором S ⊗_R M по образу I.
LaTeX
$$$$ \text{tensorQuotMapSMulEquivTensorQuot}(I) : ((S ⊗_R M) / (I.map (algebraMap R S) · ⊤)) \cong_S S ⊗_R (M / (I · ⊤)). $$$$
Lean4
/-- Let `R` be a commutative ring, `S` be an `R`-algebra, `I` is be ideal of `R`,
then `S ⊗[R] M ⧸ I(S ⊗[R] M)` is isomorphic to `S ⊗[R] (M ⧸ IM)` as `S` modules. -/
noncomputable def tensorQuotMapSMulEquivTensorQuot (I : Ideal R) :
((S ⊗[R] M) ⧸ I.map (algebraMap R S) • (⊤ : Submodule S (S ⊗[R] M))) ≃ₗ[S] S ⊗[R] (M ⧸ (I • (⊤ : Submodule R M))) :=
(tensorQuotEquivQuotSMul (S ⊗[R] M) (I.map (algebraMap R S))).symm ≪≫ₗ TensorProduct.comm S (S ⊗[R] M) _ ≪≫ₗ
AlgebraTensorModule.cancelBaseChange R S S _ M ≪≫ₗ
AlgebraTensorModule.congr (I.qoutMapEquivTensorQout S) (LinearEquiv.refl R M) ≪≫ₗ
AlgebraTensorModule.assoc R R S S _ M ≪≫ₗ
(TensorProduct.comm R _ M).baseChange R S _ _ ≪≫ₗ
(tensorQuotEquivQuotSMul M I).baseChange R S _ _
