map_tmul — Mathlib

English

For any g: M → M' in R-modules and s ∈ S, the map on tensors commutes with g: (extendScalars f).map g (s ⊗ m) = s ⊗ g m.

Русский

Для любого g: M → M' в категории модулей над R и любого s ∈ S, отображение на тензоре удовлетворяет: (extendScalars f).map g (s ⊗ m) = s ⊗ g m.

LaTeX

$$$(\extendScalars f).map\ g\ (s \otimes_{R,f} m) = s \otimes_{R,f} g\,m$$$

Lean4

@[simp]
theorem map_tmul {M M' : ModuleCat.{v} R} (g : M ⟶ M') (s : S) (m : M) :
    (extendScalars f).map g (s ⊗ₜ[R,f] m) = s ⊗ₜ[R,f] g m :=
  rfl

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