id_tensorHom_id — Mathlib

English

Tensoring identity morphisms gives the identity on the tensor product: 1_{X1} ⊗ 1_{X2} = 1_{X1 ⊗ X2}.

Русский

Тензоризация тождественных морфизмов даёт тождественный морфизм на тензорном произведении.

LaTeX

$$$\mathbf{1}_{X_1} \otimes \mathbf{1}_{X_2} = \mathbf{1}_{X_1 \otimes X_2}$$$

Lean4

theorem id_tensorHom_id (X₁ X₂ : Dial C) : (𝟙 X₁ ⊗ₘ 𝟙 X₂ : _ ⟶ _) = 𝟙 (X₁ ⊗ X₂ : Dial C) := by cat_disch

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