extendScalarsComp_hom_app_one_tmul

English

For a chain of rings, the map on the tmul basis element 1 ⊗ m under extendScalarsComp is exactly the nested tmul: 1 ⊗ 1 ⊗ m, reflecting the compatibilities of successive scalar extensions.

Русский

Для последовательности колец отображение на элементе базиса 1 ⊗ m через extendScalarsComp даёт вложение 1 ⊗ 1 ⊗ m, отражающее совместимости последовательных расширений скаляров.

LaTeX

$$$$ (\extendScalarsComp f_{12} f_{23}).\mathrm{hom}.app M ( (1) \otimes m ) = (1) \otimes (1) \otimes m. $$$$

Lean4

theorem extendScalarsComp_hom_app_one_tmul (M : ModuleCat R₁) (m : M) :
    (extendScalarsComp f₁₂ f₂₃).hom.app M ((1 : R₃) ⊗ₜ m) = (1 : R₃) ⊗ₜ[R₂,f₂₃] ((1 : R₂) ⊗ₜ[R₁,f₁₂] m) :=
  by
  rw [← extendRestrictScalarsAdj_homEquiv_apply, homEquiv_extendScalarsComp]
  rfl

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