English
There is a canonical isomorphism between QuotSMulTop r M' ⊗ M and QuotSMulTop r (M' ⊗ M).
Русский
Существует каноническое изоморфизм между QuotSMulTop r M' ⊗ M и QuotSMulTop r (M' ⊗ M).
LaTeX
$$$$ (QuotSMulTop r M') \otimes_R M \cong_R QuotSMulTop r (M' \otimes_R M) $$$$
Lean4
/-- Let `R` be a commutative ring, `M` be an `R`-module, `S` be an `R`-algebra, then
`S ⊗[R] (M/rM)` is isomorphic to `(S ⊗[R] M)⧸r(S ⊗[R] M)` as `S`-modules. -/
noncomputable def algebraMapTensorEquivTensorQuotSMulTop (S : Type*) [CommRing S] [Algebra R S] :
QuotSMulTop ((algebraMap R S) r) (S ⊗[R] M) ≃ₗ[S] S ⊗[R] QuotSMulTop r M :=
Submodule.quotEquivOfEq _ _ (by simp [Ideal.map_span, ideal_span_singleton_smul]) ≪≫ₗ
tensorQuotMapSMulEquivTensorQuot M S (Ideal.span { r }) ≪≫ₗ
(Submodule.quotEquivOfEq _ _ (ideal_span_singleton_smul r _)).baseChange R S _ _
