hom_tensorHom — Mathlib

English

The hom component of the tensor of two morphisms equals the tensor product of their hom components: (f ⊗ g).hom = f.hom ⊗ g.hom.

Русский

Гом-компонента тензорного отображения равна тензорному произведению гомоморфизмов: (f ⊗ g).hom = f.hom ⊗ g.hom.

LaTeX

$$$ (f \\otimes g).hom = \\operatorname{TensorProduct.map}(f.hom, g.hom) $$$

Lean4

theorem hom_tensorHom {K L M N : ModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) :
    (f ⊗ₘ g).hom = TensorProduct.map f.hom g.hom :=
  rfl

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