tensorObj — Mathlib

English

The tensor product of categories C and D is canonically identified with the Cartesian product of C and D considered as a category: C ⊗ D ≅ Cat.of(C × D).

Русский

Тензорное произведение категорий C и D естественно эквивалентно категории C × D, рассмотривая как категорию: C ⊗ D ≅ Cat.of(C × D).

LaTeX

$$$C \otimes D = \mathrm{Cat.of}(C \times D)$$$

Lean4

theorem tensorObj (C : Cat) (D : Cat) : C ⊗ D = Cat.of (C × D) :=
  rfl

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