English
A compatibility formula for tmul and mk' shows how the tensor product interacts with the localization numerator.
Русский
Совместная формула для tmul и mk' описывает взаимоотношение между тензорным произведением и локализационной числителем.
LaTeX
$$$IsLocalization.tmul\_mk'(M, s, x, y)$$$
Lean4
/-- `S⁻¹M ⊗[R] N = S⁻¹(M ⊗[R] N)`. -/
instance rTensor (g : M →ₗ[A] M') [h : IsLocalizedModule S g] :
IsLocalizedModule S (AlgebraTensorModule.rTensor R N g) :=
by
let Aₚ := Localization S
letI : Module Aₚ M' := (IsLocalizedModule.iso S g).symm.toAddEquiv.module Aₚ
haveI : IsScalarTower A Aₚ M' := (IsLocalizedModule.iso S g).symm.isScalarTower Aₚ
haveI : IsScalarTower R Aₚ M' :=
IsScalarTower.of_algebraMap_smul <| fun r x ↦ by simp [IsScalarTower.algebraMap_apply R A Aₚ]
rw [isLocalizedModule_iff_isBaseChange (S := S) (A := Aₚ)] at h ⊢
exact isBaseChange_tensorProduct_map _ h
