tensorHom_hom

Mathlib.Algebra.Category.CommAlgCat.Monoidal

URI: https://scilib.ai/kg/mathlib#CommAlgCat.tensorHom_hom

English

The tensor product morphism corresponds to the map on homs after tensoring.

Русский

Отображение гомоморфизмов в тензорном произведении соответствует отображению гомоморфизмов.

LaTeX

$$$ (f \otimes g).hom = map f.hom g.hom $$$

Lean4

@[simp]
theorem tensorHom_hom (f : A ⟶ C) (g : B ⟶ D) : (f ⊗ₘ g).hom = map f.hom g.hom :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru