tensorQuotEquivQuotSMul_symm_comp_mkQ

English

There is a natural linear isomorphism between M ⊗ (R/I) and M/(I ⊤) via tensoring with the quotient and passing to the quotient on M.

Русский

Существует естественный линейный изоморфизм между M ⊗ (R/I) и M/(I ⊤) через тензорирование по фактору и переход к фактор-модулю в M.

LaTeX

$$$$ M \otimes_R (R / I) \cong_R M / (I \top). $$$$

Lean4

theorem tensorQuotEquivQuotSMul_symm_comp_mkQ (I : Ideal R) :
    (tensorQuotEquivQuotSMul M I).symm ∘ₗ (I • ⊤ : Submodule R M).mkQ = (TensorProduct.mk R M (R ⧸ I)).flip 1 :=
  LinearMap.ext (tensorQuotEquivQuotSMul_symm_mk I)

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