equivTensorProduct — Mathlib

English

If A is a localization of R, tensoring two A-modules over A is the same as tensoring them over R; i.e., M1 ⊗_A M2 ≃_A M1 ⊗_R M2.

Русский

Если A — локализация от R, то тензорное произведение двух A-модулей над A эквивалентно тензорному произведению над R: M1 ⊗_A M2 ≃_A M1 ⊗_R M2.

LaTeX

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

Lean4

/-- The localization of an `R`-module `M` at a submonoid `S` is isomorphic to `S⁻¹R ⊗[R] M` as
an `S⁻¹R`-module. -/
noncomputable def equivTensorProduct : LocalizedModule S M ≃ₗ[Localization S] Localization S ⊗[R] M :=
  IsLocalizedModule.isBaseChange S (Localization S) (LocalizedModule.mkLinearMap S M) |>.equiv.symm

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