quotientTensorEquiv_apply_tmul_mk

English

Let m be a submodule of M. There is a canonical linear isomorphism between M ⊗_R (N/m) and (M ⊗_R N)/(M ⊗_R m). This map sends the pure tensor x ⊗ (y + m) to x ⊗ y + (M ⊗ m).

Русский

Пусть m ⊆ M является подпростраством. Существует каноническое линейное изоморфное отображение M ⊗_R (N/m) ≅ (M ⊗_R N)/(M ⊗_R m), которое отправляет чистый тензор x ⊗ (y + m) в x ⊗ y + (M ⊗ m).

LaTeX

$$$$ M \otimes_R (N / m) \cong_R (M \otimes_R N) / (M \otimes_R m). $$$$

Lean4

@[simp]
theorem quotientTensorEquiv_apply_tmul_mk (m : Submodule R M) (x : M) (y : N) :
    quotientTensorEquiv N m (Submodule.Quotient.mk x ⊗ₜ[R] y) = Submodule.Quotient.mk (x ⊗ₜ y) :=
  rfl

Похожие утверждения