hom_tensorHom — Mathlib

English

Tensoring morphisms corresponds to the induced homomorphism on tensor products: (f ⊗ g).hom = Algebra.TensorProduct.map f.hom g.hom.

Русский

Тензорное произведение морфизмов соответствует гомоморфизму на тензорных произведениях: (f ⊗ g).hom = Algebra.TensorProduct.map f.hom g.hom.

LaTeX

$$$$ (f \otimes_{-} g).\hom = \operatorname{Algebra.TensorProduct.map}(f.\hom, g.\hom). $$$$

Lean4

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

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