moduleTensorEquiv — Mathlib

English

There is a canonical linear equivalence between M1 ⊗_A M2 and M1 ⊗_R M2 when A is a localization of R.

Русский

Существует каноническое линейное эквивалентное отображение между M1 ⊗_A M2 и M1 ⊗_R M2 при том, что A является локализацией R.

LaTeX

$$$M_1 \otimes_A M_2 \cong_A M_1 \otimes_R M_2$$$

Lean4

/-- If `A` is a localization of `R`, tensoring two `A`-modules over `A` is the same as
tensoring them over `R`. -/
noncomputable def moduleTensorEquiv : M₁ ⊗[A] M₂ ≃ₗ[A] M₁ ⊗[R] M₂ :=
  have := tensorProduct_compatibleSMul S A M₁ M₂
  equivOfCompatibleSMul R A M₁ M₂

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