map_tmul — Mathlib

English

There is a canonical equality between the general tensor-product map and the specialized AlgebraTensorModule.map when used with coalgebra morphisms.

Русский

Существует каноническое равенство между общим отображением на тензорном произведении и специализированным AlgebraTensorModule.map для коалгебра морфизмов.

LaTeX

$$$$ map\;f\;g = AlgebraTensorModule.map (f) (g). $$$$

Lean4

@[simp]
theorem map_tmul (f : M →ₗc[S] N) (g : P →ₗc[R] Q) (x : M) (y : P) : map f g (x ⊗ₜ y) = f x ⊗ₜ g y :=
  rfl

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